Search results for "theorem-prover"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
22	Stefan Berghofer, Tobias Nipkow	Random Testing in Isabelle/HOL.	SEFM	2004	DBLP DOI BibTeX RDF
22	Sorin Lerner, Todd D. Millstein, Craig Chambers	Automatically proving the correctness of compiler optimizations.	PLDI	2003	DBLP DOI BibTeX RDF	automated correctness proofs, compiler optimization
22	Robert S. Boyer, J Strother Moore	Single-Threaded Objects in ACL2.	PADL	2002	DBLP DOI BibTeX RDF
22	Ali Habibi, Sofiène Tahar, Adel Ghazel	Formal Verification of a DSP Chip Using an Iterative Approach.	DSD	2002	DBLP DOI BibTeX RDF
22	Michael Alekhnovich, Alexander A. Razborov	Satisfiability, Branch-Width and Tseitin Tautologies.	FOCS	2002	DBLP DOI BibTeX RDF
22	Yoshihiko Futamura, Zenjiro Konishi, Robert Glück	WSDFU: Program Transformation System Based on Generalized Partial Computation.	The Essence of Computation	2002	DBLP DOI BibTeX RDF
22	Krysia Broda	A Decidable CLDS for Some Propositional Resource Logics.	Computational Logic: Logic Programming and Beyond	2002	DBLP DOI BibTeX RDF
22	J Strother Moore	Functional formal methods.	ICFP	2002	DBLP DOI BibTeX RDF	functional programming, Java Virtual Machine, microarchitecture, software verification, Common Lisp, hardware verification, mechanical theorem proving
22	Jürgen Zimmer, Michael Kohlhase	System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning.	CADE	2002	DBLP DOI BibTeX RDF
22	Graeme Smith 0001, Florian Kammüller, Thomas Santen	Encoding Object-Z in Isabelle/HOL.	ZB	2002	DBLP DOI BibTeX RDF	reference semantics, Object-Z, higher-order logic, Isabelle
22	David von Oheimb, Volkmar Lotz	Formal Security Analysis with Interacting State Machines.	ESORICS	2002	DBLP DOI BibTeX RDF
22	Pertti Kellomäki	A Structural Embedding of Ocsid in PVS.	TPHOLs	2001	DBLP DOI BibTeX RDF
22	Steffen Helke, Thomas Santen	Mechanized Analysis of Behavioral Conformance in the Eiffel Base Libraries.	FME	2001	DBLP DOI BibTeX RDF
22	Francisco-Jesús Martín-Mateos, José-Antonio Alonso, María-José Hidalgo, José-Luis Ruiz-Reina	Verifying an Applicative ATP Using Multiset Relations.	EUROCAST	2001	DBLP DOI BibTeX RDF
22	Bart Jacobs 0001, Erik Poll	A Logic for the Java Modeling Language JML.	FASE	2001	DBLP DOI BibTeX RDF
22	Ricardo Caferra, Nicolas Peltier, François Puitg	Emphasizing Human Techniques in Automated Geometry Theorem Proving: A Practical Realization.	Automated Deduction in Geometry	2000	DBLP DOI BibTeX RDF	Automated geometric reasoning, model (counter-example) building, proof structuring with diagrams, analogy, computer assisted learning
22	Herman Geuvers, Freek Wiedijk, Jan Zwanenburg	Equational Reasoning via Partial Reflection.	TPHOLs	2000	DBLP DOI BibTeX RDF
22	Stephan Merz	Weak Alternating Automata in Isabelle/HOL.	TPHOLs	2000	DBLP DOI BibTeX RDF
22	John Harrison 0001	High-Level Verification Using Theorem Proving and Formalized Mathematics.	CADE	2000	DBLP DOI BibTeX RDF
22	William McCune, Olga Shumsky	System Description: IVY.	CADE	2000	DBLP DOI BibTeX RDF
22	Cornelia Pusch	Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL.	TACAS	1999	DBLP DOI BibTeX RDF
22	John M. Rushby, Sam Owre, Natarajan Shankar	Subtypes for Specifications: Predicate Subtyping in PVS.	IEEE Trans. Software Eng.	1998	DBLP DOI BibTeX RDF	typechecking, Formal methods, consistency, type systems, specification languages, subtypes, PVS
22	Amy P. Felty, Douglas J. Howe, Frank A. Stomp	Protocol Verification in Nuprl.	CAV	1998	DBLP DOI BibTeX RDF
22	Christoph Schwarzweller	Mizar Correctness Proofs of Generic Fraction Field Arithmetic.	Generic Programming	1998	DBLP DOI BibTeX RDF
22	Susanne Graf, Hassen Saïdi	Construction of Abstract State Graphs with PVS.	CAV	1997	DBLP DOI BibTeX RDF	state graph exploration, theorem proving, abstract interpretation
22	Pertti Kellomäki	Verification of Reactive Systems Using DisCo and PVS.	FME	1997	DBLP DOI BibTeX RDF
22	Mary Cryan, Allan Ramsay	Constructing a Normal Form for Property Theory.	CADE	1997	DBLP DOI BibTeX RDF
22	David von Oheimb, Thomas F. Gritzner	RALL: Machine-Supported Proofs for Relation Algebra.	CADE	1997	DBLP DOI BibTeX RDF	interactive and automatic theorem proving, atom structure, Relation algebra, Isabelle
22	Uwe Egly, Thomas Rath	On the Practical Value of Different Definitional Translations to Normal Form.	CADE	1996	DBLP DOI BibTeX RDF
22	Steve Linton, Ursula Martin, Péter Pröhle, Duncan Shand	Algebra and Automated Deduction.	CADE	1996	DBLP DOI BibTeX RDF
22	Konrad Slind	AC Unification in HOL90.	HUG	1993	DBLP DOI BibTeX RDF
22	Joseph A. Goguen, Rod M. Burstall	Institutions: Abstract Model Theory for Specification and Programming.	J. ACM	1992	DBLP DOI BibTeX RDF
22	Christian B. Suttner, Wolfgang Ertel	Automatic Acquisition of Search Guiding Heuristics.	CADE	1990	DBLP DOI BibTeX RDF	learning, heuristics, features, Automated theorem proving, back-propagation, connectionism, evaluation functions, model elimination
22	Warren A. Hunt Jr., Bishop Brock	The Verification of a Bit-slice ALU.	Hardware Specification, Verification and Synthesis	1989	DBLP DOI BibTeX RDF
22	Hantao Zhang 0001, Deepak Kapur, Mukkai S. Krishnamoorthy	A Mechanizable Induction Principle for Equational Specifications.	CADE	1988	DBLP DOI BibTeX RDF
22	Jack Minker, Arcot Rajasekar	Procedural Interpretation of Non-Horn Logic Programs.	CADE	1988	DBLP DOI BibTeX RDF	generalized closed world assumption, non-horn programs, procedural interpretation, support-for-negation, logic programming, negation
22	Shan Chi, Lawrence J. Henschen	Recursive Query Answering with Non-Horn Clauses.	CADE	1988	DBLP DOI BibTeX RDF
22	Tanel Tammet	The resolution program, able to decide some solvable classes.	Conference on Computer Logic	1988	DBLP DOI BibTeX RDF
22	Barbara A. Smith, Ralph W. Wilkerson, Gerald E. Peterson	Automated Circuit Diagnosis Using First Order Logic Tools.	IEA/AIE (Vol. 1)	1988	DBLP DOI BibTeX RDF
19	Erik Reeber, Warren A. Hunt Jr.	A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA).	IJCAR	2006	DBLP DOI BibTeX RDF
19	John M. Rushby	Tutorial: Automated Formal Methods with PVS, SAL, and Yices.	SEFM	2006	DBLP DOI BibTeX RDF
19	John M. Rushby	An Evidential Tool Bus.	ICFEM	2005	DBLP DOI BibTeX RDF
19	Peter Baumgartner 0001, Ulrich Furbach, Margret Groß-Hardt, Alex Sinner	Living Book - Deduction, Slicing, and Interaction.	J. Autom. Reason.	2004	DBLP DOI BibTeX RDF	knowledge management, e-learning, knowledge representation, theorem proving
19	Ruben Gamboa, John R. Cowles	A Mechanical Proof of the Cook-Levin Theorem.	TPHOLs	2004	DBLP DOI BibTeX RDF
19	Tomás Recio, Francisco Botana	Where the Truth Lies (in Automatic Theorem Proving in Elementary Geometry).	ICCSA (2)	2004	DBLP DOI BibTeX RDF
19	Vu Ha, Murali Rangarajan, Darren D. Cofer, Harald Rueß, Bruno Dutertre	Feature-Based Decomposition of Inductive Proofs Applied to Real-Time Avionics Software: An Experience Report.	ICSE	2004	DBLP DOI BibTeX RDF
19	John Harrison 0001	Formal Verification at Intel.	LICS	2003	DBLP DOI BibTeX RDF
19	Stefan Berghofer	A Constructive Proof of Higman's Lemma in Isabelle.	TYPES	2003	DBLP DOI BibTeX RDF
19	Miroslav Popovic, Vladimir Kovacevic, Ivan Velikic	A Formal Software Verification Concept Based on Automated Theorem Proving and Reverse Engineering.	ECBS	2002	DBLP DOI BibTeX RDF	formal software verification, fault-tolerant and robust software, mission-critical embedded software, reverse engineering, automated theorem proving, predicate calculus
19	Simon Colton	The HR Program for Theorem Generation.	CADE	2002	DBLP DOI BibTeX RDF
19	Steve Roach, Jeffrey Van Baalen	Experience Report on Automated Procedure Construction for Deductive Synthesis.	ASE	2002	DBLP DOI BibTeX RDF
19	Jun Sawada, Ruben Gamboa	Mechanical Verification of a Square Root Algorithm Using Taylor's Theorem.	FMCAD	2002	DBLP DOI BibTeX RDF
19	Noboru Matsuda, Kurt VanLehn	A Reification of a Strategy for Geometry Theorem Proving.	Intelligent Tutoring Systems	2000	DBLP DOI BibTeX RDF
19	Rajeev Goré, Lan Duy Nguyen	CardKt: Automated Multi-modal Deduction on Java Cards for Multi-application Security.	Java Card Workshop	2000	DBLP DOI BibTeX RDF	security of multi-application smart cards, applications of logics of knowledge and belief, modal theorem proving, tense logics
19	V. K. Pisini, Sofiène Tahar, Paul Curzon, Otmane Aït Mohamed, Xiaoyu Song	Formal hardware verification by integrating HOL and MDG.	ACM Great Lakes Symposium on VLSI	2000	DBLP DOI BibTeX RDF
19	Andrew Ireland, Mike Jackson 0003, Gordon Reid	Interactive Proof Critics.	Formal Aspects Comput.	1999	DBLP DOI BibTeX RDF	Proof patching, Inductive proof, User interfaces, Theorem proving, Proof planning
19	Panagiotis Manolios, Kedar S. Namjoshi, Robert Summers	Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation.	CAV	1999	DBLP DOI BibTeX RDF
19	Naren Narasimhan, Ranga Vemuri	On the Effectiveness of Theorem Proving Guided Discovery of Formal Assertions for a Register Allocator in a High-Level Synthesis System.	TPHOLs	1998	DBLP DOI BibTeX RDF
19	Henrik Ejersbo Jensen, Nancy A. Lynch	A Proof of Burns N-Process Mutual Exclusion Algorithm Using Abstraction.	TACAS	1998	DBLP DOI BibTeX RDF
19	Daniel S. Korn, Christoph Kreitz	Deciding Intuitionistic Propositional Logic via Translation into Classical Logic.	CADE	1997	DBLP DOI BibTeX RDF
19	Robert Matzinger	Computational Representations of Herbrand Models Using Grammars.	CSL	1996	DBLP DOI BibTeX RDF
19	Wolfgang Ertel	OR-Parallel Theorem Proving with Random Competition.	LPAR	1992	DBLP DOI BibTeX RDF	random competition, SETHEO, theorem proving, speedup, OR-parallelism, random search, model elimination
19	Ricardo Caferra, Stéphane Demri	Semantic Entailment in Non Classical Logics Based on Proofs Found in Classical Logic.	CADE	1992	DBLP DOI BibTeX RDF
19	Alan M. Frisch, Richard B. Scherl	A Constraint Logic Approach to Modal Deduction.	JELIA	1990	DBLP DOI BibTeX RDF
19	Ewing L. Lusk, William McCune, Ross A. Overbeek	Logic Machine Architecture: Inference Mechanisms.	CADE	1982	DBLP DOI BibTeX RDF
18	Sean McLaughlin, Frank Pfenning	Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic.	LPAR	2008	DBLP DOI BibTeX RDF
18	Laura I. Meikle, Jacques D. Fleuriot	Prover's Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD-B.	CAV	2008	DBLP DOI BibTeX RDF
18	Laura I. Meikle, Jacques D. Fleuriot	Combining Isabelle and QEPCAD-B in the Prover's Palette.	AISC/MKM/Calculemus	2008	DBLP DOI BibTeX RDF
18	Behzad Akbarpour, Lawrence C. Paulson	Extending a Resolution Prover for Inequalities on Elementary Functions.	LPAR	2007	DBLP DOI BibTeX RDF
18	Andreas Abel 0001, Thierry Coquand, Ulf Norell	Connecting a Logical Framework to a First-Order Logic Prover.	FroCoS	2005	DBLP DOI BibTeX RDF
18	Laurence Cholvy, Christophe Garion	Answering Queries Addressed to Several Databases According to a Majority Merging Approach.	J. Intell. Inf. Syst.	2004	DBLP DOI BibTeX RDF	majority merging, logic, deductive databases, database merging
18	Laurence Cholvy, Christophe Garion	Answering Queries Addressed to Several Databases: A Query Evaluator which Implements a Majority Merging Approach.	ISMIS	2002	DBLP DOI BibTeX RDF	majority merging, logic, Database merging
18	Hans de Nivelle	Splitting Through New Proposition Symbols.	LPAR	2001	DBLP DOI BibTeX RDF
18	Rajeev Goré, Phuong Thê Nguyên	CardS4: Modal Theorem Proving on Java Smartcards.	E-smart	2001	DBLP DOI BibTeX RDF	security of mobile code, modal deduction
18	Stephan Schulz 0001	System Abstract: E 0.61.	IJCAR	2001	DBLP DOI BibTeX RDF
18	Florent Jacquemard, Michaël Rusinowitch, Laurent Vigneron	Compiling and Verifying Security Protocols.	LPAR	2000	DBLP DOI BibTeX RDF
18	Kenneth L. McMillan	Some Strategies for Proving Theorems with a Model Checker.	LICS	2000	DBLP DOI BibTeX RDF
18	A. K. Bhattacharjee, Gopa Sen, S. D. Dhodapkar, Kundapur Karunakar, Basant Rajan, R. K. Shyamasundar	A System for Object Code Validation.	FTRTFT	2000	DBLP DOI BibTeX RDF
18	Stephan Schulz 0001	System Abstract: E 0.3.	CADE	1999	DBLP DOI BibTeX RDF
18	Johann Schumann	Automatic Verification of Cryptographic Protocols with SETHEO.	CADE	1997	DBLP DOI BibTeX RDF
18	Deepak Kapur, Mahadevan Subramaniam	Mechanizing Verification of Arithmetic Circuits: SRT Division.	FSTTCS	1997	DBLP DOI BibTeX RDF
18	Chih-Hung Wu, Shie-Jue Lee	On parallelism of hyper-linking theorem proving: a preliminary report.	ICPADS	1996	DBLP DOI BibTeX RDF	hyper-linking theorem proving, hyper-linking proof procedure, phase-level, clause-level, literal-level, search level parallelism, parallel strategies, parallel algorithms, parallelism, artificial intelligence, parallel architectures, theorem proving
18	Scott Hazelhurst, Carl-Johan H. Seger	Composing Symbolic Trajectory Evaluation Results.	CAV	1994	DBLP DOI BibTeX RDF
18	Peter Baumgartner 0001, Ulrich Furbach	PROTEIN: A PROver with a Theory Extension INterface.	CADE	1994	DBLP DOI BibTeX RDF
18	Larry M. Hines	The Central Variable Strategy of Str+ve.	CADE	1992	DBLP DOI BibTeX RDF
18	David M. Goldschlag	Mechanically Verifying Safety and Liveness Properties of Delay Insensitive Circuits.	CAV	1991	DBLP DOI BibTeX RDF
18	Larry M. Hines	Str+ve-Subset: The Str+ve-based Subset Prover.	CADE	1990	DBLP DOI BibTeX RDF
18	Norihisa Suzuki, Kiyoshi Ishihata	Implementation of an Array Bound Checker.	POPL	1977	DBLP DOI BibTeX RDF
15	Mark E. Stickel	Building Theorem Provers.	CADE	2009	DBLP DOI BibTeX RDF
15	Giampaolo Bella, Pietro Liò	Formal Analysis of the Genetic Toggle.	CMSB	2009	DBLP DOI BibTeX RDF
15	Amine Chaieb, Tobias Nipkow	Proof Synthesis and Reflection for Linear Arithmetic.	J. Autom. Reason.	2008	DBLP DOI BibTeX RDF	Proof synthesis, Linear arithmetic, Reflection
15	Sascha Böhme, K. Rustan M. Leino, Burkhart Wolff	HOL-Boogie - An Interactive Prover for the Boogie Program-Verifier.	TPHOLs	2008	DBLP DOI BibTeX RDF
15	Ralph Matthes	Nested Datatypes with Generalized Mendler Iteration: Map Fusion and the Example of the Representation of Untyped Lambda Calculus with Explicit Flattening.	MPC	2008	DBLP DOI BibTeX RDF
15	Andrea Asperti, Wilmer Ricciotti	About the Formalization of Some Results by Chebyshev in Number Theory.	TYPES	2008	DBLP DOI BibTeX RDF
15	Alexander Krauss 0001	Pattern minimization problems over recursive data types.	ICFP	2008	DBLP DOI BibTeX RDF	complexity, pattern matching, theorem proving
15	Ulrich Furbach, Ingo Glöckner, Hermann Helbig, Björn Pelzer	LogAnswer - A Deduction-Based Question Answering System (System Description).	IJCAR	2008	DBLP DOI BibTeX RDF
15	Andriy Dunets, Gerhard Schellhorn, Wolfgang Reif	Bounded Relational Analysis of Free Data Types.	TAP	2008	DBLP DOI BibTeX RDF	SAT checking, model checking, verification, formal methods, theorem proving, First-order logic, abstract data types
15	Rob Verhoeven, Francien Dechesne	Verifying Multi-party Authentication Using Rank Functions and PVS.	Formal Aspects in Security and Trust	2008	DBLP DOI BibTeX RDF
15	Haiyan Xiong, Paul Curzon, Sofiène Tahar, Ann Blandford	Providing a formal linkage between MDG and HOL.	Formal Methods Syst. Des.	2007	DBLP DOI BibTeX RDF	Verification system correctness, Hybrid verification systems, Formal hardware verification, Usability verification
15	Ralph Matthes, Martin Strecker	Verification of the Redecoration Algorithm for Triangular Matrices.	TYPES	2007	DBLP DOI BibTeX RDF