Search results for "theorem-proving"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
34	Alan Bundy	The Use of Explicit Plans to Guide Inductive Proofs.	CADE	1988	DBLP DOI BibTeX RDF	inductive proofs, formal methods, planning, theorem proving, automatic programming, Proof plans
33	Maarten de Mol, Marko C. J. D. van Eekelen	A Proof Tool Dedicated to Clean - The First Prototype.	AGTIVE	1999	DBLP DOI BibTeX RDF
33	Peter B. Andrews	Transforming Matings into Natural Deduction Proofs.	CADE	1980	DBLP DOI BibTeX RDF
32	Camilo Rocha, José Meseguer 0001	Theorem Proving Modulo Based on Boolean Equational Procedures.	RelMiCS	2008	DBLP DOI BibTeX RDF
32	Fredrik Lindblad, Marcin Benke	A Tool for Automated Theorem Proving in Agda.	TYPES	2004	DBLP DOI BibTeX RDF
32	Jürgen Zimmer, Louise A. Dennis	Inductive Theorem Proving and Computer Algebra in the MathWeb Software Bus.	AISC	2002	DBLP DOI BibTeX RDF
32	Peter B. Andrews, Chad E. Brown	Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic.	CADE	2000	DBLP DOI BibTeX RDF
32	Jürgen Dingel, Thomas Filkorn	Model Checking for Infinite State Systems Using Data Abstraction, Assumption-Commitment Style reasoning and Theorem Proving.	CAV	1995	DBLP DOI BibTeX RDF
32	Peter V. Homeier, David F. Martin	Trustworthy Tools for Trustworthy Programs: A Verified Verification Condition Generator.	TPHOLs	1994	DBLP DOI BibTeX RDF
32	Mark D. Aagaard, Miriam Leeser, Phillip J. Windley	Toward a Super Duper Hardware Tactic.	HUG	1993	DBLP DOI BibTeX RDF
32	Hantao Zhang 0001, Deepak Kapur	First-Order Theorem Proving Using Conditional Rewrite Rules.	CADE	1988	DBLP DOI BibTeX RDF
32	Jieh Hsiang, Michaël Rusinowitch	A New Method for Establishing Refutational Completeness in Theorem Proving.	CADE	1986	DBLP DOI BibTeX RDF
32	Alexander Leitsch	Decision Procedures and Model Building, or How to Improve Logical Information in Automated Deduction.	FTP (LNCS Selection)	1998	DBLP DOI BibTeX RDF
31	Geoff Sutcliffe, Christoph Benzmüller, Chad E. Brown, Frank Theiss	Progress in the Development of Automated Theorem Proving for Higher-Order Logic.	CADE	2009	DBLP DOI BibTeX RDF
31	Shuaiqiang Wang, Jiancheng Wan, Jinkui Hou	OR-ATP: An Operation Refinement Approach As a Process of Automatic Theorem Proving.	SNPD (3)	2007	DBLP DOI BibTeX RDF
31	Greta Yorsh, Thomas Ball, Mooly Sagiv	Testing, abstraction, theorem proving: better together!	ISSTA	2006	DBLP DOI BibTeX RDF	fabricated states, state-based coverage, testing, abstraction, program analysis, abstract interpretation, coverage, theorem prover, software fault injection, adequacy criteria
31	Yves Bertot, Laurent Théry	Dependent Types, Theorem Proving, and Applications for a Verifying Compiler.	VSTTE	2005	DBLP DOI BibTeX RDF
31	Alexander Koller, Ralph Debusmann, Malte Gabsdil, Kristina Striegnitz	Put My Galakmid Coin into the Dispenser and Kick It: Computational Linguistics and Theorem Proving in a Computer Game.	J. Log. Lang. Inf.	2004	DBLP DOI BibTeX RDF	text adventures, generation, description logic, parsing, theorem provers, reference resolution, dependency grammar
31	Hasan Amjad	Programming a Symbolic Model Checker in a Fully Expansive Theorem Prover.	TPHOLs	2003	DBLP DOI BibTeX RDF
31	Stefan Edelkamp, Peter Leven	Directed Automated Theorem Proving.	LPAR	2002	DBLP DOI BibTeX RDF
31	Eric Neufeld	Clue as a Testbed for Automated Theorem Proving.	AI	2002	DBLP DOI BibTeX RDF
31	Douglas J. Howe	Interactive Theorem Proving Using Type Theory.	CSL	1999	DBLP DOI BibTeX RDF
31	Jacques D. Fleuriot, Lawrence C. Paulson	A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton's Principia.	CADE	1998	DBLP DOI BibTeX RDF
31	Rimvydas Ruksenas, Joakim von Wright	A Tool for Data Refinement.	TPHOLs	1998	DBLP DOI BibTeX RDF
31	Sten Agerholm, Jacob Frost	Towards an Integrated CASE and Theorem Proving Tool for VDM-SL.	FME	1997	DBLP DOI BibTeX RDF
31	Sten Agerholm, Jacob Frost	An Isabelle-Based Theorem Prover for VDM-SL.	TPHOLs	1997	DBLP DOI BibTeX RDF
31	Susanne Graf, Hassen Saïdi	Verifying Invariants Using theorem Proving.	CAV	1996	DBLP DOI BibTeX RDF
31	Edmund M. Clarke, Steven M. German, Xudong Zhao 0005	Verifying the SRT Division Algorithm Using Theorem Proving Techniques.	CAV	1996	DBLP DOI BibTeX RDF
31	Thomas Kolbe, Christoph Walther	Termination of Theorem Proving by Reuse.	CADE	1996	DBLP DOI BibTeX RDF
31	Amy P. Felty, Douglas J. Howe	Tactic Theorem Proving with Refinement-Tree Proofs and Metavariables.	CADE	1994	DBLP DOI BibTeX RDF
31	Hardi Hungar	Combining Model Checking and Theorem Proving to Verify Parallel Processes.	CAV	1993	DBLP DOI BibTeX RDF
31	David A. Basin, Seán Matthews	A Conservative Extension of First-order Logic and Its Application to Theorem Proving.	FSTTCS	1993	DBLP DOI BibTeX RDF
31	Jeffrey J. Joyce, Carl-Johan H. Seger	The HOL-Voss System: Model-Checking inside a General-Purpose Theorem-Prover.	HUG	1993	DBLP DOI BibTeX RDF
31	Wilfred Z. Chen	Tactic-based Theorem Proving and Knowledge-based Forward Chaining: an Experiment with Nuprl and Ontic.	CADE	1992	DBLP DOI BibTeX RDF
30	K. Rustan M. Leino	Invariants on Demand.	SEFM	2005	DBLP DOI BibTeX RDF
30	David Déharbe, Silvio Ranise	Satisfiability solving for software verification.	Int. J. Softw. Tools Technol. Transf.	2009	DBLP DOI BibTeX RDF	Equational theorem proving, Boolean solving, Theory reasoning, Software verification
30	Christoph Sprenger 0001, David A. Basin	Cryptographically-Sound Protocol-Model Abstractions.	CSF	2008	DBLP DOI BibTeX RDF	cryptographic soundness, formal methods, theorem proving, Cryptographic protocols, simulatability
30	Tertia Hörne, John A. van der Poll	Planning as model checking: the performance of ProB vs NuSMV.	SAICSIT	2008	DBLP DOI BibTeX RDF	tableaux theorem proving, model checking, planning, satisfiability, BDDs, constraint logic programming
30	Youngsik Kim, Nazanin Mansouri	Automated formal verification of scheduling with speculative code motions.	ACM Great Lakes Symposium on VLSI	2008	DBLP DOI BibTeX RDF	formal verification, high level synthesis, automated theorem-proving, speculation
30	Achim D. Brucker, Burkhart Wolff	HOL-OCL: A Formal Proof Environment for UML/OCL.	FASE	2008	DBLP DOI BibTeX RDF	holocl, ocl, Formal Method, Theorem Proving, uml
30	Qiang Guan, Long Wang 0001, Bican Xia, Lu Yang, Wensheng Yu, Zhenbing Zeng	Solution to the Generalized Champagne Problem on simultaneous stabilization of linear systems.	Sci. China Ser. F Inf. Sci.	2007	DBLP DOI BibTeX RDF	simultaneous stabilization, Champagne Problem, Generalized Champagne Problem, inequality-type theorem, stabilization, linear systems, automated theorem proving, complex analysis
30	Fadoua Ghourabi, Tetsuo Ida, Hidekazu Takahashi, Mircea Marin, Asem Kasem	Logical and algebraic view of Huzita's origami axioms with applications to computational origami.	SAC	2007	DBLP DOI BibTeX RDF	constraint solving, first-order predicate logic, origami, geometric theorem proving
30	Matthew Might	Logic-flow analysis of higher-order programs.	POPL	2007	DBLP DOI BibTeX RDF	LFA, abstract counting, abstract garbage collection, environment analysis, gamma-CFA first-order logic, logic-flow analysis, static analysis, theorem proving, lambda calculus, CPS
30	Sven Beyer, Christian Jacobi 0002, Daniel Kröning, Dirk Leinenbach, Wolfgang J. Paul	Putting it all together - Formal verification of the VAMP.	Int. J. Softw. Tools Technol. Transf.	2006	DBLP DOI BibTeX RDF	Complete microprocessor verification, Tomasulo scheduler, Cache memory interface, Model checking, Formal methods, Theorem proving, Floating point unit
30	June Andronick, Boutheina Chetali, Christine Paulin-Mohring	Formal Verification of Security Properties of Smart Card Embedded Source Code.	FM	2005	DBLP DOI BibTeX RDF	Source code verification, Security, Formal Methods, Theorem Proving, Smart Card
30	David Cachera, Thomas P. Jensen, David Pichardie, Gerardo Schneider	Certified Memory Usage Analysis.	FM	2005	DBLP DOI BibTeX RDF	certified memory analysis, Program analysis, theorem proving, constraint solving
30	Rajesh Kumar 0005, Bruce H. Krogh, Peter H. Feiler	An Ontology-Based Approach to Heterogeneous Verification of Embedded Control Systems.	HSCC	2005	DBLP DOI BibTeX RDF	ontology, theorem proving, knowledge base, knowledge integration
30	Alma L. Juarez Dominguez, Nancy A. Day	Compositional reasoning for port-based distributed systems.	ASE	2005	DBLP DOI BibTeX RDF	DFC, model checking, theorem proving, compositional verification
30	Johan Bos	Computational Semantics in Discourse: Underspecification, Resolution, and Inference.	J. Log. Lang. Inf.	2004	DBLP DOI BibTeX RDF	discourse representation theory, scope ambiguities, structural ambiguities, theorem proving, inference, discourse analysis, computational semantics, underspecification, lexical ambiguities
30	Sigrid Gürgens, Javier López 0001, René Peralta 0001	Analysis of e-commerce protocols: Adapting a traditional technique.	Int. J. Inf. Sec.	2003	DBLP DOI BibTeX RDF	Electronic commerce, Cryptographic protocol, Security analysis, Automatic theorem proving, Protocol validation
30	Yihong Wu 0002, Zhanyi Hu	The Invariant Representations of a Quadric Cone and a Twisted Cubic.	IEEE Trans. Pattern Anal. Mach. Intell.	2003	DBLP DOI BibTeX RDF	quadric cone, twisted cubic, computer vision, Automated theorem proving, invariant representation
30	Geoff Sutcliffe, Christian B. Suttner	The CADE-18 ATP System Competition.	J. Autom. Reason.	2003	DBLP DOI BibTeX RDF	competition, automated theorem proving
30	Vlad Rusu	Compositional Verification of an ATM Protocol.	FME	2003	DBLP DOI BibTeX RDF	SSCOP protocol, abstraction, theorem proving, Compositionality, PVS
30	Eric Gascard, Laurence Pierre	Mechanical Verification of Hypercube Algorithms.	IPDPS	2002	DBLP DOI BibTeX RDF	Parallel algorithms, Formal verification, MPI, Hypercube, Theorem proving, Cayley graphs
30	J Strother Moore	A Grand Challenge Proposal for Formal Methods: A Verified Stack.	10th Anniversary Colloquium of UNU/IIST	2002	DBLP DOI BibTeX RDF	simulation, modeling, model checking, theorem proving, software verification, hardware verification
30	Behzad Akbarpour, Abdelkader Dekdouk, Sofiène Tahar	Formalization of Cadence SPW Fixed-Point Arithmetic in HOL.	IFM	2002	DBLP DOI BibTeX RDF	SPW, Theorem-Proving, Signal Processing, Floating-point, Fixed-point, HOL
30	José Oscar Olmedo-Aguirre, Guillermo Morales-Luna	Indeed : Interactive Deduction on Horn Clause Theories.	IBERAMIA	2002	DBLP DOI BibTeX RDF	Horn clause theories, interaction, Logic programming, automated theorem proving
30	J Strother Moore	Rewriting for Symbolic Execution of State Machine Models.	CAV	2001	DBLP DOI BibTeX RDF	microprocessor simulation, pipelined machine, verification, theorem proving, Hardware modeling
30	Tristan Cazenave	Abstract Proof Search.	Computers and Games	2000	DBLP DOI BibTeX RDF	Computer Go, Capture Game, Search, Theorem Proving
30	Gonzalo Escalada-Imaz, Rodolfo Torres-Velázquez	Complexity Issues in the Davis and Putnam Scheme.	AIMSA	2000	DBLP DOI BibTeX RDF	Computational Complexity, Search, Theorem Proving, Automated Reasoning
30	Guilherme Bittencourt, Isabel Tonin	A Proof Strategy Based on a Dual Representation.	AISC	2000	DBLP DOI BibTeX RDF	inference strategy, dual transformation, Topic: Logic and Symbolic Computing, theorem proving, First-order logic
30	Christoph Kern, Mark R. Greenstreet	Formal verification in hardware design: a survey.	ACM Trans. Design Autom. Electr. Syst.	1999	DBLP DOI BibTeX RDF	language containment, model checking, formal methods, formal verification, case studies, theorem proving, survey, hardware verification
30	Axel Dold	Software Development in PVS Using Generic Development Steps.	Generic Programming	1998	DBLP DOI BibTeX RDF	generic development steps, transformational software development, formal verification, mechanized theorem proving
30	Andreas Zeller	Versioning System Models Through Description Logic.	SCM	1998	DBLP DOI BibTeX RDF	Deduction and theorem proving, Software architecture, Version control, Software configuration management, Knowledge representation formalisms and methods
30	Mats Per Erik Heimdahl, Barbara J. Czerny	Using PVS to analyze hierarchical state-based requirements for completeness and consistency.	HASE	1996	DBLP DOI BibTeX RDF	hierarchical state based requirements specifications, input sequence, analysis procedures, large real world requirements specification, hierarchical state based language, Requirements State Machine Language, Prototype Verification System, theorem proving component, spurious error reports, formal specifications, robustness, consistency, program verification, completeness, Binary Decision Diagrams, BDDs, PVS, interactive environment, formal proofs, RSML
30	Ming-Yuan Zhu, Xiao-Bai Mo	Mechanical synthesis of a unification algorithm in PowerEpsilon.	COMPSAC	1995	DBLP DOI BibTeX RDF	PowerEpsilon, constructive type theory, proof development system, formal program development system, formal specification, specification, programming, theorem proving, programming theory, type theory, unification algorithm, mechanical synthesis
30	Naima Brown, Dominique Méry	A Proof Environment for Concurrent Programs.	FME	1993	DBLP DOI BibTeX RDF	formal specifications, concurrency, program verification, Automated theorem proving, B, Unity
30	R. Ramesh 0001, I. V. Ramakrishnan	Nonlinear Pattern Matching in Trees.	J. ACM	1992	DBLP DOI BibTeX RDF	nonlinear pattern matching, theorem proving, normalization, rewriting
30	Carsten Fuhs, Jürgen Giesl, Michael Parting, Peter Schneider-Kamp, Stephan Swiderski	Proving Termination by Dependency Pairs and Inductive Theorem Proving.	J. Autom. Reason.	2011	DBLP DOI BibTeX RDF
30	Jieh Hsiang, Michaël Rusinowitch	Proving Refutational Completeness of Theorem-Proving Strategies: The Transfinite Semantic Tree Method.	J. ACM	1991	DBLP DOI BibTeX RDF
27	Martin Suda 0001, Geoff Sutcliffe, Patrick Wischnewski, Manuel Lamotte-Schubert, Gerard de Melo	External Sources of Axioms in Automated Theorem Proving.	KI	2009	DBLP DOI BibTeX RDF
27	Stephan Swiderski, Michael Parting, Jürgen Giesl, Carsten Fuhs, Peter Schneider-Kamp	Termination Analysis by Dependency Pairs and Inductive Theorem Proving.	CADE	2009	DBLP DOI BibTeX RDF
27	Konstantine Arkoudas, Olin Shivers	Trusted Theorem Proving: A Case Study in SLD-Resolution.	ISoLA	2008	DBLP DOI BibTeX RDF
27	Makarius Wenzel, Lawrence C. Paulson, Tobias Nipkow	The Isabelle Framework.	TPHOLs	2008	DBLP DOI BibTeX RDF
27	Yves Bertot	A Short Presentation of Coq.	TPHOLs	2008	DBLP DOI BibTeX RDF
27	Russell O'Connor	Certified Exact Transcendental Real Number Computation in Coq.	TPHOLs	2008	DBLP DOI BibTeX RDF
27	Ashish Tiwari 0001, Sumit Gulwani	Logical Interpretation: Static Program Analysis Using Theorem Proving.	CADE	2007	DBLP DOI BibTeX RDF
27	Lukas Bulwahn, Alexander Krauss 0001, Tobias Nipkow	Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL.	TPHOLs	2007	DBLP DOI BibTeX RDF
27	James Reynolds	Automatically Translating Type and Function Definitions from HOL to ACL2.	TPHOLs	2007	DBLP DOI BibTeX RDF
27	Eugenio Roanes-Macías, Eugenio Roanes-Lozano	A Maple Package for Automatic Theorem Proving and Discovery in 3D-Geometry.	Automated Deduction in Geometry	2006	DBLP DOI BibTeX RDF
27	Panagiotis Manolios	Refinement and Theorem Proving.	SFM	2006	DBLP DOI BibTeX RDF
27	Sa Cui, Kevin Donnelly, Hongwei Xi	ATS: A Language That Combines Programming with Theorem Proving.	FroCoS	2005	DBLP DOI BibTeX RDF
27	Steven Obua	Proving Bounds for Real Linear Programs in Isabelle/HOL.	TPHOLs	2005	DBLP DOI BibTeX RDF
27	Maxim Makatchev, Pamela W. Jordan, Kurt VanLehn	Abductive Theorem Proving for Analyzing Student Explanations to Guide Feedback in Intelligent Tutoring Systems.	J. Autom. Reason.	2004	DBLP DOI BibTeX RDF	intelligent tutoring systems, abductive reasoning, qualitative physics
27	Thomas F. Melham	Integrating Model Checking and Theorem Proving in a Reflective Functional Language.	IFM	2004	DBLP DOI BibTeX RDF
27	Harald Ganzinger, Konstantin Korovin	Integrating Equational Reasoning into Instantiation-Based Theorem Proving.	CSL	2004	DBLP DOI BibTeX RDF
27	Konstantine Arkoudas, Sarfraz Khurshid, Darko Marinov, Martin C. Rinard	Integrating Model Checking and Theorem Proving for Relational Reasoning.	RelMiCS	2003	DBLP DOI BibTeX RDF
27	Harald Ganzinger, Konstantin Korovin	New Directions in Instantiation-Based Theorem Proving.	LICS	2003	DBLP DOI BibTeX RDF
27	Michael Norrish	Complete Integer Decision Procedures as Derived Rules in HOL.	TPHOLs	2003	DBLP DOI BibTeX RDF
27	Ricky W. Butler	Formal Methods at NASA Langley.	TPHOLs	2002	DBLP DOI BibTeX RDF
27	Stephan Schulz 0001	Learning Search Control Knowledge for Equational Theorem Proving.	KI/ÖGAI	2001	DBLP DOI BibTeX RDF
27	Reiner Hähnle, Ryuzo Hasegawa, Yasuyuki Shirai	Moder Generation Theorem Proving with Finite Interval Constraints.	Computational Logic	2000	DBLP DOI BibTeX RDF
27	John M. Rushby	Theorem Proving for Verification.	MOVEP	2000	DBLP DOI BibTeX RDF
27	M. Randall Holmes	A Strong and Mechanizable Grand Logic.	TPHOLs	2000	DBLP DOI BibTeX RDF
27	Hanne Gottliebsen	Transcendental Functions and Continuity Checking in PVS.	TPHOLs	2000	DBLP DOI BibTeX RDF
27	John M. Rushby	Integrated Formal Verification: Using Model Checking with Automated Abstraction, Invariant Generation, and Theorem Proving.	SPIN	1999	DBLP DOI BibTeX RDF
27	Sergei N. Artëmov	On Explicit Reflection in Theorem Proving and Formal Verification.	CADE	1999	DBLP DOI BibTeX RDF
27	Vincent Zammit	On the Implementation of an Extensible Declarative Proof Language.	TPHOLs	1999	DBLP DOI BibTeX RDF
27	Wu Wen-Tsün	Automatic Geometry Theorem-Proving and Automatic Geometry Problem-Solving.	Automated Deduction in Geometry	1998	DBLP DOI BibTeX RDF
27	Viorica Sofronie-Stokkermans	Resolution-Based Theorem Proving for SHn-Logics.	FTP (LNCS Selection)	1998	DBLP DOI BibTeX RDF