SatyendraBanjare / plt-formal-methods-resources
Curated List of Research Focused Reading Materials & Videos for Learning about Programming Language Theory Research, Formal Methods and their application in some most active computer Science fields.
☆52Updated 5 years ago
Related projects ⓘ
Alternatives and complementary repositories for plt-formal-methods-resources
- Appendix of "Principles of Abstract Interpretation", P. Cousot, MIT Press, 2021, containing the proofs and the solutions of exercises not…☆40Updated 3 years ago
- Here we collect worldwide courses teaching formal methods☆33Updated 5 years ago
- A Verified Compiler for Gallina, Written in Gallina☆136Updated 3 months ago
- ☆26Updated last week
- Communication between Coq and SAT/SMT solvers☆157Updated 2 months ago
- ☆13Updated 4 months ago
- A web page with resources for teaching with formal methods and tools.☆14Updated last year
- A Library for Representing Recursive and Impure Programs in Coq☆204Updated last month
- A function definition package for Coq☆223Updated last week
- CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory☆218Updated last week
- slides for the book "Principles od Abstract Interpretation", P. Cousot, MIT Press, 2021☆14Updated last year
- TriCera: a model checker for C programs☆18Updated last week
- Coq plugin embedding elpi☆139Updated this week
- Selected Papers of Dana S. Scott☆155Updated 5 months ago
- Definition of the Viper intermediate verification language.☆79Updated this week
- Collection of resources for research concerning Machine Learning and Formal Methods.☆77Updated 2 years ago
- A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainer=@palmskog]☆319Updated 3 months ago
- Ltac2 tutorial☆42Updated 2 years ago
- Jupyter notebooks for tutorial on the Z3 SMT solver☆154Updated last year
- Verification-condition-generation-based verifier for the Viper intermediate verification language.☆30Updated last week
- Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintaine…☆69Updated 9 months ago
- Armv8 Native Code Symbolic Simulator in Lean☆63Updated last week
- VeriFFI: Verified Foreign Function Interface for connecting Coq programs to C programs at the operational and specification/verification …☆38Updated 4 months ago
- A library of mechanised undecidability proofs in the Coq proof assistant.☆111Updated last month
- An automatic theorem prover in OCaml for typed higher-order logic with equality and datatypes, based on superposition+rewriting; and Logt…☆139Updated last month
- ☆223Updated 3 months ago
- PL conference deadline countdowns☆52Updated 2 weeks ago
- The Eldarica model checker☆80Updated last month
- Apron Numerical Abstract Domain Library☆114Updated 3 months ago
- SampCert : Verified Differential Privacy☆65Updated 3 months ago