- Proof Synthesis and Reflection for Linear Arithmetic Amine Chaieb Tobias Nipkow Fri 02 March 2012
- The TPTP Problem Library and Associated Infrastructure Geoff Sutcliffe Fri 02 March 2012
- MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions Behzad Akbarpour Lawrence Charles Paulson Fri 02 March 2012
- The HOL Light Theory of Euclidean Space John Harrison Fri 02 March 2012
- Formalization of Bernstein Polynomials and Applications to Global Optimization César Muñoz Anthony Narkawicz Fri 02 March 2012
- textquotedblleftDecision Procedures: An Algorithmic Point of View,textquotedblright by Daniel Kroening and Ofer Strichman, Springer-Verlag, 2008 Clark Barrett Fri 02 March 2012
- A Heuristic Prover for Real Inequalities Jeremy Avigad Robert Y. Lewis Cody Roux Fri 02 March 2012
- Eisbach: A Proof Method Language for Isabelle Daniel Matichuk Toby Murray Makarius Wenzel Fri 02 March 2012
- A Learning-Based Fact Selector for Isabelle/HOL Jasmin Christian Blanchette David Greenaway Cezary Kaliszyk Daniel Kühlwein Josef Urban Fri 02 March 2012
- A Decision Procedure for (Co)datatypes in SMT Solvers Andrew Reynolds Jasmin Christian Blanchette Fri 02 March 2012
- Analyzing Program Termination and Complexity Automatically with AProVE Jürgen Giesl Cornelius Aschermann Marc Brockschmidt Fabian Emmes Florian Frohn Carsten Fuhs Jera Hensel Carsten Otto Martin Plücker Peter Schneider-Kamp Thomas Ströder Stephanie Swiderski René Thiemann Fri 02 March 2012
- Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic Thomas Ströder Jürgen Giesl Marc Brockschmidt Florian Frohn Carsten Fuhs Jera Hensel Peter Schneider-Kamp Cornelius Aschermann Fri 02 March 2012
- Visibly Linear Temporal Logic Laura Bozzelli César Sánchez Fri 02 March 2012
- Refinement to Imperative HOL Peter Lammich Fri 02 March 2012
- A Consistent Foundation for Isabelle/HOL Ondřej Kunčar Andrei Popescu Fri 02 March 2012
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality Jasmin Christian Blanchette Mathias Fleury Peter Lammich Christoph Weidenbach Fri 02 March 2012
- Canonicity for Cubical Type Theory Simon Huber Fri 02 March 2012
- Mechanized Metatheory Revisited Dale Miller Fri 02 March 2012
- A Verified Generational Garbage Collector for CakeML Adam Sandberg Ericsson Magnus O. Myreen Johannes AAman Pohjola Fri 02 March 2012
- A Learning-Based Approach to Synthesizing Invariants for Incomplete Verification Engines Daniel Neider P. Madhusudan Shambwaditya Saha Pranav Garg Daejun Park Fri 02 March 2012
Library Size: 13G (12949 entries),
Last Updated: Apr 11, 2026, 18:05:34,
Build Time: N/A
