Search results for "theorem-prover"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
23	Gordon Stewart 0001, Lennart Beringer, Andrew W. Appel	Verified heap theorem prover by paramodulation.	ICFP	2012	DBLP DOI BibTeX RDF
23	Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois	Tableaux Modulo Theories Using Superdeduction - An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover.	IJCAR	2012	DBLP DOI BibTeX RDF
23	Hao Xu 0011	How To Efficiently Implement An OSHL-Based Automatic Theorem Prover.		2012	DOI RDF
23	Erik Zawadzki, Geoffrey J. Gordon, André Platzer	An Instantiation-Based Theorem Prover for First-Order Programming.	AISTATS	2011	DBLP BibTeX RDF
23	Ángel Mora 0001, Emilio Muñoz-Velasco, Joanna Golinska-Pilarek	Implementing a relational theorem prover for modal logic.	Int. J. Comput. Math.	2011	DBLP DOI BibTeX RDF
23	Tjark Weber	SMT solvers: new oracles for the HOL theorem prover.	Int. J. Softw. Tools Technol. Transf.	2011	DBLP DOI BibTeX RDF
23	David S. Hardin, Julien Schmaltz (eds.)	Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2011, Austin, Texas, USA, November 3-4, 2011.	ACL2	2011	DBLP DOI BibTeX RDF
23	Jussi Rintanen	Constructing Conditional Plans by a Theorem-Prover	CoRR	2011	DBLP BibTeX RDF
23	Ralph-Johan Back, Johannes Eriksson	An Exercise in Invariant-based Programming with Interactive and Automatic Theorem Prover Support	ThEdu	2011	DBLP DOI BibTeX RDF
23	Osman Hasan, Sofiène Tahar	Reasoning about conditional probabilities in a higher-order-logic theorem prover.	J. Appl. Log.	2011	DBLP DOI BibTeX RDF
23	Krystof Hoder, Laura Kovács, Andrei Voronkov	Case Studies on Invariant Generation Using a Saturation Theorem Prover.	MICAI (1)	2011	DBLP DOI BibTeX RDF
23	Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi	The Matita Interactive Theorem Prover.	CADE	2011	DBLP DOI BibTeX RDF
23	Juan Antonio Navarro Pérez, Andrey Rybalchenko	Separation logic + superposition calculus = heap theorem prover.	PLDI	2011	DBLP DOI BibTeX RDF
23	Régis Alenda, Nicola Olivetti	CSymLean: A Theorem Prover for the Logic CSL over Symmetric Minspaces.	TABLEAUX	2011	DBLP DOI BibTeX RDF
23	Magnus O. Myreen, Jared Davis	A Verified Runtime for a Verified Theorem Prover.	ITP	2011	DBLP DOI BibTeX RDF
23	Simon Foster 0001, Georg Struth	Integrating an Automated Theorem Prover into Agda.	NASA Formal Methods	2011	DBLP DOI BibTeX RDF
23	Harsh Raju Chamarthi, Panagiotis Manolios	Automated specification analysis using an interactive theorem prover.	FMCAD	2011	DBLP BibTeX RDF
23	Andrea Asperti, Maria Emilia Maietti, Claudio Sacerdoti Coen, Giovanni Sambin, Silvio Valentini	Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita.	Calculemus/MKM	2011	DBLP DOI BibTeX RDF
23	Freek Verbeek, Julien Schmaltz	Formal verification of a deadlock detection algorithm	ACL2	2011	DBLP DOI BibTeX RDF
23	Peter Reid, Ruben Gamboa	Implementing an Automatic Differentiator in ACL2	ACL2	2011	DBLP DOI BibTeX RDF
23	Sol Swords, Jared Davis	Bit-Blasting ACL2 Theorems	ACL2	2011	DBLP DOI BibTeX RDF
23	Matt Kaufmann, J Strother Moore	How Can I Do That with ACL2? Recent Enhancements to ACL2	ACL2	2011	DBLP DOI BibTeX RDF
23	Peter-Michael Seidel	Formal Verification of an Iterative Low-Power x86 Floating-Point Multiplier with Redundant Feedback	ACL2	2011	DBLP DOI BibTeX RDF
23	Mike Dahlin, Ryan Johnson 0003, Robert Bellarmine Krug, Michael McCoyd, William D. Young	Toward the Verification of a Simple Hypervisor	ACL2	2011	DBLP DOI BibTeX RDF
23	John R. Cowles, Ruben Gamboa	Verifying Sierpinski and Riesel Numbers in ACL2	ACL2	2011	DBLP DOI BibTeX RDF
23	Harsh Raju Chamarthi, Peter C. Dillinger, Matt Kaufmann, Panagiotis Manolios	Integrating Testing and Interactive Theorem Proving	ACL2	2011	DBLP DOI BibTeX RDF
23	Scott Uk-Jin Lee, Gillian Dobbie, Jing Sun 0002, Lindsay Groves	Theorem prover approach to semistructured data design.	Formal Methods Syst. Des.	2010	DBLP DOI BibTeX RDF
23	Gang Chen	Formalization of a Parameterized Parallel Adder Within the Coq Theorem Prover.	IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.	2010	DBLP DOI BibTeX RDF
23	Tim vor der Brück, Hermann Helbig	Meronymy Extraction Using An Automated Theorem Prover.	J. Lang. Technol. Comput. Linguistics	2010	DBLP BibTeX RDF
23	Behzad Akbarpour, Lawrence C. Paulson	MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions.	J. Autom. Reason.	2010	DBLP DOI BibTeX RDF
23	Sana Stojanovic, Vesna Pavlovic, Predrag Janicic	A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs.	Automated Deduction in Geometry	2010	DBLP DOI BibTeX RDF
23	Andrew Butterfield	Saoithín: A Theorem Prover for UTP.	UTP	2010	DBLP DOI BibTeX RDF
23	Tim vor der Brück, Holger Stenzhorn	Logical Ontology Validation Using an Automatic Theorem Prover.	ECAI	2010	DBLP DOI BibTeX RDF
23	Thomas Bouton, Diego Caminha, David Déharbe, Pascal Fontaine	GridTPT: a distributed platform for Theorem Prover Testing.	PAAR@IJCAR	2010	DBLP DOI BibTeX RDF
23	Konstantin Korovin, Christoph Sticksel	iProver-Eq: An Instantiation-Based Theorem Prover with Equality.	IJCAR	2010	DBLP DOI BibTeX RDF
23	Dominic Richards, David R. Lester	A Prototype Embedding of Bluespec SystemVerilog in the PVS Theorem Prover.	NASA Formal Methods	2010	DBLP BibTeX RDF
23	Maksym Bortin	An approach to the extension of a theorem prover by advanced structuring mechanisms.		2010	RDF
23	Régis Alenda, Nicola Olivetti, Gian Luca Pozzato	CSL-lean: A Theorem-prover for the Logic of Comparative Concept Similarity.	M4M	2009	DBLP DOI BibTeX RDF
23	Ricky W. Butler	Formalization of the Integral Calculus in the PVS Theorem Prover.	J. Formaliz. Reason.	2009	DBLP DOI BibTeX RDF
23	Hicham Bensaid, Ricardo Caferra, Nicolas Peltier	Dei: A Theorem Prover for Terms with Integer Exponents.	CADE	2009	DBLP DOI BibTeX RDF
23	Shimmi Asokan, G. Santhosh Kumar, N. Jaya Lal	Modeling of ALFA Programs Using PVS Theorem Prover.	ARTCom	2009	DBLP DOI BibTeX RDF
23	Laura Kovács, Andrei Voronkov	Finding Loop Invariants for Programs over Arrays Using a Theorem Prover.	SYNASC	2009	DBLP DOI BibTeX RDF
23	Zurab Khasidashvili, Mahmoud Kinanah, Andrei Voronkov	Verifying equivalence of memories using a first order logic theorem prover.	FMCAD	2009	DBLP DOI BibTeX RDF
23	John Byrnes, Michael Buchanan, Michael Ernst, Philip Miller, Chris Roberts, Robert Keller	Visualizing Proof Search for Theorem Prover Development.	UITP@TPHOLs	2008	DBLP DOI BibTeX RDF
23	Andrew Gacek	The Abella Interactive Theorem Prover (System Description).	IJCAR	2008	DBLP DOI BibTeX RDF
23	Sa'ed Abed, Otmane Aït Mohamed, Ghiath Al Sammane	The Performance of Combining Multiway Decision Graphs and HOL Theorem Prover.	FDL	2008	DBLP DOI BibTeX RDF
23	Patrick Barlatier, Richard Dapoigny	A Theorem Prover with Dependent Types for Reasoning about Actions.	STAIRS	2008	DBLP DOI BibTeX RDF
23	Bo Guo, Mahadevan Subramaniam	Formal Change Impact Analyses of Extended Finite State Machines Using a Theorem Prover.	SEFM	2008	DBLP DOI BibTeX RDF
23	Marco Cadoli, Toni Mancini	Using a Theorem Prover for Reasoning on Constraint Problems.	Appl. Artif. Intell.	2007	DBLP DOI BibTeX RDF
23	Jolyon Clulow	Robbing the Bank with a Theorem Prover - (Transcript of Discussion).	Security Protocols Workshop	2007	DBLP DOI BibTeX RDF
23	Paul Youn, Ben Adida, Mike Bond, Jolyon Clulow, Jonathan Herzog, Amerson Lin, Ronald L. Rivest, Ross J. Anderson	Robbing the Bank with a Theorem Prover - (Abstract).	Security Protocols Workshop	2007	DBLP DOI BibTeX RDF
23	Ralph Butler, Chrisila C. Pettey	A Bilingual Theorem Prover for Evaluating HPC Systems.	PDPTA	2007	DBLP BibTeX RDF
23	Cezary Kaliszyk, Freek Wiedijk	Certified Computer Algebra on Top of an Interactive Theorem Prover.	Calculemus/MKM	2007	DBLP DOI BibTeX RDF
23	Louise A. Dennis	Enhancing Theorem Prover Interfaces with Program Slice Information.	UITP@FLoC	2006	DBLP DOI BibTeX RDF
23	Kamal Aboul-Hosn, Dexter Kozen	KAT-ML: an interactive theorem prover for Kleene algebra with tests.	J. Appl. Non Class. Logics	2006	DBLP DOI BibTeX RDF
23	Panagiotis Manolios, Matthew Wilding (eds.)	Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006	ACL2	2006	DBLP BibTeX RDF
23	Anduo Wang, Fei He 0001, Ming Gu 0001, Xiaoyu Song	Verifying Java Programs By Theorem Prover HOL.	COMPSAC (1)	2006	DBLP DOI BibTeX RDF
23	David L. Rager	Adding parallelism capabilities to ACL2.	ACL2	2006	DBLP DOI BibTeX RDF	pand, parallel ACL2, pcall, plet, por, granularity, functional language
23	Jared Davis	Memories: array-like records for ACL2.	ACL2	2006	DBLP DOI BibTeX RDF	MBE, fixnum optimization, linear address spaces, arrays, records, ACL2
23	John R. Cowles, Ruben Gamboa	Unique factorization in ACL2: Euclidean domains.	ACL2	2006	DBLP DOI BibTeX RDF	Boyer-Moore logic, Euclidean domains, unique factorization, ACL2
23	Matt Kaufmann, J Strother Moore	Double rewriting for equivalential reasoning in ACL2.	ACL2	2006	DBLP DOI BibTeX RDF	double-rewrite, verification, formal methods, rewriting, congruences, equivalence relations
23	Ruben Gamboa, John R. Cowles	Implementing a cost-aware evaluator for ACL2 expressions.	ACL2	2006	DBLP DOI BibTeX RDF	ACL2 evaluator, function cost, evaluators
23	Jared Davis	Reasoning about ACL2 file input.	ACL2	2006	DBLP DOI BibTeX RDF	UTF-8, file input, ACL2, unicode, exhaustive testing
23	Sandip Ray	Quantification in tail-recursive function definitions.	ACL2	2006	DBLP DOI BibTeX RDF	formal methods, logic, ACL2, conservativity, skolemization
23	Sol Swords, William R. Cook	Soundness of the simply typed lambda calculus in ACL2.	ACL2	2006	DBLP DOI BibTeX RDF	lambda-calculus, soundness, ACL2
23	Robert S. Boyer, Warren A. Hunt Jr.	Function memoization and unique object representation for ACL2 functions.	ACL2	2006	DBLP DOI BibTeX RDF	ACL2 workshop, function memoization, hash CONS, hash CONSing, Lisp, ACL2
23	Tony Hoare	The ideal of verified software.	ACL2	2006	DBLP DOI BibTeX RDF
23	David A. Greve	Parameterized congruences in ACL2.	ACL2	2006	DBLP DOI BibTeX RDF
23	Michael J. C. Gordon, Warren A. Hunt Jr., Matt Kaufmann, James Reynolds	An embedding of the ACL2 logic in HOL.	ACL2	2006	DBLP DOI BibTeX RDF	HOL4, proof oracle, sound translation, verification, formal methods, logic, first-order logic, higher-order logic, ACL2, HOL
23	Warren A. Hunt Jr., Erik Reeber	A SAT-based procedure for verifying finite state machines in ACL2.	ACL2	2006	DBLP DOI BibTeX RDF	satisfiability solving, theorem proving, hardware verification, ACL2
23	Lee Pike, Mark Shields, John Matthews	A verifying core for a cryptographic language compiler.	ACL2	2006	DBLP DOI BibTeX RDF	cryptography, certification, optimizing compiler, ACL2, high-assurance, certifying compiler, verifying compiler
23	Warren A. Hunt Jr., Serita M. Nelesen	Phylogenetic trees in ACL2.	ACL2	2006	DBLP DOI BibTeX RDF	ACL2, phylogenetics
23	David S. Hardin, Eric W. Smith, William D. Young	A robust machine code proof framework for highly secure applications.	ACL2	2006	DBLP DOI BibTeX RDF	cryptography, theorem proving, certification, symbolic simulation, ACL2, high-assurance, processor modeling
23	Tjark Weber	Integrating a SAT Solver with an LCF-style Theorem Prover.	PDPAR@CAV	2005	DBLP DOI BibTeX RDF
23	David Déharbe, Silvio Ranise, Jorgiano Vidal	Distributing the Workload in a Lazy Theorem-Prover.	SBMF	2005	DBLP DOI BibTeX RDF
23	Kenneth L. McMillan	An interpolating theorem prover.	Theor. Comput. Sci.	2005	DBLP DOI BibTeX RDF
23	David Detlefs, Greg Nelson, James B. Saxe	Simplify: a theorem prover for program checking.	J. ACM	2005	DBLP DOI BibTeX RDF	Theorem proving, decision procedures, program checking
23	Tom Ridge, James Margetson	A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic.	TPHOLs	2005	DBLP DOI BibTeX RDF
23	K. Rustan M. Leino, Madan Musuvathi, Xinming Ou	A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover.	TACAS	2005	DBLP DOI BibTeX RDF
23	Marco Cadoli, Toni Mancini	Using a Theorem Prover for Reasoning on Constraint Problems.	AI*IA	2005	DBLP DOI BibTeX RDF
23	Choon Kyu Kim	Exploiting parallelism: highly competitive semantic tree theorem prover.	Int. J. Comput. Math.	2004	DBLP DOI BibTeX RDF
23	Nicola Olivetti, Gian Luca Pozzato, Camilla Schwind	A Sequent Calculus and a Theorem Prover for Standard Conditional Logics	CoRR	2004	DBLP BibTeX RDF
23	Peter Kullmann, Sandra A. Sandri	An annotated logic theorem prover for an extended possibilistic logic.	Fuzzy Sets Syst.	2004	DBLP DOI BibTeX RDF
23	Tom Ridge	A Mechanically Verified, Efficient, Sound and Complete Theorem Prover For First Order Logic.	Arch. Formal Proofs	2004	DBLP BibTeX RDF
23	Yasuyuki Shirai, Ryuzo Hasegawa	Answer Set Computation Based on a Minimal Model Generation Theorem Prover.	PRICAI	2004	DBLP DOI BibTeX RDF
23	Arnold Binas, John K. Slaney	Semantically Guiding a First-Order Theorem Prover with a Soft Model.	AAAI	2004	DBLP BibTeX RDF
23	John K. Slaney, Arnold Binas, David Price	Guiding a Theorem Prover with Soft Constraints.	ECAI	2004	DBLP BibTeX RDF
23	Daniel Winterstein	Dr.Doodle: A Diagrammatic Theorem Prover.	IJCAR Doctoral Programme	2004	DBLP BibTeX RDF
23	Zhen Li	An implementation of a tableau theorem prover for modal logics.	IJCAR Doctoral Programme	2004	DBLP BibTeX RDF
23	Thomas Hillenbrand	Citius altius fortius: Lessons learned from the Theorem Prover WALDMEISTER.	FTP	2003	DBLP DOI BibTeX RDF
23	Choon Kyu Kim, Monty Newborn	Competitive Semantic Tree Theorem Prover with Resolutions.	PVM/MPI	2003	DBLP DOI BibTeX RDF
23	Stephan Schulz 0001	E - a brainiac theorem prover.	AI Commun.	2002	DBLP BibTeX RDF
23	Kahlil Hodgson, John K. Slaney	TPTP, CASC and the development of a semantically guided theorem prover.	AI Commun.	2002	DBLP BibTeX RDF
23	Dominique Pastre	Strong and weak points of the MUSCADET theorem prover - examples from CASC-JC.	AI Commun.	2002	DBLP BibTeX RDF
23	Paul Z. Kolano	Proof assistance for real-time systems using an interactive theorem prover.	Theor. Comput. Sci.	2002	DBLP DOI BibTeX RDF
23	Orieta Celiku, Joakim von Wright	Theorem Prover Support for Precondition and Correctness Calculation.	ICFEM	2002	DBLP DOI BibTeX RDF
23	Jamie Shield, Ian J. Hayes, David A. Carrington	Using Theory Interpretation to Mechanise the Reals in a Theorem Prover.	CATS	2001	DBLP DOI BibTeX RDF
23	Ortrun Ibens, Marc Fuchs	An Automated Theorem Prover Based on Connection Tableau Calculi with Disjunctive Constraints.	Int. J. Artif. Intell. Tools	2001	DBLP DOI BibTeX RDF
23	M. Randall Holmes, Jim Alves-Foss	The Watson Theorem Prover.	J. Autom. Reason.	2001	DBLP DOI BibTeX RDF
23	Chih-Hung Wu, Shie-Jue Lee	Parallelization of a Hyper-Linking-Based Theorem Prover.	J. Autom. Reason.	2001	DBLP DOI BibTeX RDF