Search results for "theorem-prover"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
15	Björn Pelzer, Christoph Wernhard	System Description: E-KRHyper.	CADE	2007	DBLP DOI BibTeX RDF
15	Todd Deshane, Wenjin Hu, Patty Jablonski, Hai Lin 0005, Christopher Lynch, Ralph Eric McGregor	Encoding First Order Proofs in SAT.	CADE	2007	DBLP DOI BibTeX RDF
15	Achim D. Brucker, Burkhart Wolff	Test-Sequence Generation with Hol-TestGen with an Application to Firewall Testing.	TAP	2007	DBLP DOI BibTeX RDF	symbolic test case generations, theorem proving, computer security, black box testing, Isabelle/HOL, test sequence generation
15	Osman Hasan, Sofiène Tahar	Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function.	IFM	2007	DBLP DOI BibTeX RDF	Higher-Order-Logic, Interactive Theorem Proving, HOL, Probabilistic Systems, Cumulative Distribution Function
15	José Luis Freire-Nistal, Enrique Freire Brañas, Antonio Blanco Ferro, David Cabrero Souto	On the Representation of Imperative Programs in a Logical Framework.	EUROCAST	2007	DBLP DOI BibTeX RDF
15	J Strother Moore	Inductive assertions and operational semantics.	Int. J. Softw. Tools Technol. Transf.	2006	DBLP DOI BibTeX RDF	Theorem proving, JVM, Software verification, Verification condition
15	J. Christian Attiogbé	Multi-process Systems Analysis Using Event B: Application to Group Communication Systems.	ICFEM	2006	DBLP DOI BibTeX RDF	Event B, Dynamic Architecture, Group Communication Systems, Property verification
15	Jim Woodcock 0001, Leo Freitas	Z/Eves and the Mondex Electronic Purse.	ICTAC	2006	DBLP DOI BibTeX RDF	electronic finance, software archaeology, the Z notation, Z/Eves, security, refinement, theorem proving, smart cards, Grand Challenge, Verified Software Repository, Mondex
15	Viktor Kuncak, Martin C. Rinard	An overview of the Jahob analysis system: project goals and current status.	IPDPS	2006	DBLP DOI BibTeX RDF
15	Thomas Tuerk, Klaus Schneider 0001, Mike Gordon	Model Checking PSL Using HOL and SMV.	Haifa Verification Conference	2006	DBLP DOI BibTeX RDF
15	Li Ye, Junliang Chen	Automatic Composition of Semantic Web Services - A Theorem Proof Approach.	ASWC	2006	DBLP DOI BibTeX RDF	Automatic Theorem Proof, Deductive Program Synthesis, Semantic Web Services, Automatic Service Composition
15	Andrei Voronkov	Inconsistencies in Ontologies.	JELIA	2006	DBLP DOI BibTeX RDF
15	Panagiotis Manolios, Daron Vroon 0001	Integrating static analysis and general-purpose theorem proving for termination analysis.	ICSE	2006	DBLP DOI BibTeX RDF	static analysis, theorem proving, termination, liveness, ACL2
15	Pedro Quaresma, Predrag Janicic	Integrating Dynamic Geometry Software, Deduction Systems, and Theorem Repositories.	MKM	2006	DBLP DOI BibTeX RDF
15	Steve Roach, Jeffrey Van Baalen	Automated Procedure Construction for Deductive Synthesis.	Autom. Softw. Eng.	2005	DBLP DOI BibTeX RDF	synthesis, procedures, deductive, decision, partial deduction
15	John Harrison 0001	A HOL Theory of Euclidean Space.	TPHOLs	2005	DBLP DOI BibTeX RDF
15	Jim Woodcock 0001, Ana Cavalcanti 0001, Leonardo Freitas	Operational Semantics for Model Checking Circus.	FM	2005	DBLP DOI BibTeX RDF
15	K. Rustan M. Leino, Francesco Logozzo	Loop Invariants on Demand.	APLAS	2005	DBLP DOI BibTeX RDF
15	Oliver Ray	The Need for Ancestor Resolution When Answering Queries in Horn Clause Logic.	ICLP	2005	DBLP DOI BibTeX RDF
15	Chad E. Brown	Reasoning in Extensional Type Theory with Equality.	CADE	2005	DBLP DOI BibTeX RDF
15	Ittai Balaban, Amir Pnueli, Lenore D. Zuck	Shape Analysis by Predicate Abstraction.	VMCAI	2005	DBLP DOI BibTeX RDF
15	Yannick Chevalier, Laurent Vigneron	Strategy for Verifying Security Protocols with Unbounded Message Size.	Autom. Softw. Eng.	2004	DBLP DOI BibTeX RDF	intruder model, automatic strategies, verification, security protocols, flaw detection
15	Toh Ne Win, Michael D. Ernst, Stephen J. Garland, Dilsun Kirli Kaynar, Nancy A. Lynch	Using simulated execution in verifying distributed algorithms.	Int. J. Softw. Tools Technol. Transf.	2004	DBLP DOI BibTeX RDF	Invariant detection, Static analysis, Theorem proving, Dynamic analysis
15	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
15	Daniel Winterstein, Alan Bundy, Corin A. Gurr, Mateja Jamnik	An Experimental Comparison of Diagrammatic and Algebraic Logics.	Diagrams	2004	DBLP DOI BibTeX RDF
15	Jerzy Marcinkowski, Jan Otop, Grzegorz Stelmaszek	On a Semantic Subsumption Test.	LPAR	2004	DBLP DOI BibTeX RDF
15	Sandip Ray, Warren A. Hunt Jr.	Deductive Verification of Pipelined Machines Using First-Order Quantification.	CAV	2004	DBLP DOI BibTeX RDF
15	Alexander Krupp, Wolfgang Müller 0003, Ian Oliver	Formal Refinement and Model Checking of an Echo Cancellation Unit.	DATE	2004	DBLP DOI BibTeX RDF
15	Yue Tang, Jin Song Dong, Jing Sun 0002, Brendan P. Mahony	Reasoning about Semantic Web in Isabelle/HOL.	APSEC	2004	DBLP DOI BibTeX RDF
15	Jinghai Rao, Peep Küngas, Mihhail Matskin	Logic-based Web Services Composition: From Service Description to Process Model.	ICWS	2004	DBLP DOI BibTeX RDF
15	Terrance Swift	Deduction in Ontologies via ASP.	LPNMR	2004	DBLP DOI BibTeX RDF
15	Simon Colton, Andreas Meier 0002, Volker Sorge, Roy L. McCasland	Automatic Generation of Classification Theorems for Finite Algebras.	IJCAR	2004	DBLP DOI BibTeX RDF
15	Tjark Weber	Towards Mechanized Program Verification with Separation Logic.	CSL	2004	DBLP DOI BibTeX RDF	Separation Logic, Interactive Theorem Proving, Formal Program Verification
15	Juan Carlos López Pimentel, Raúl Monroy	A Rippling-Based Difference Reduction Technique to Automatically Prove Security Protocol Goals.	IBERAMIA	2004	DBLP DOI BibTeX RDF
15	Sandeep S. Kulkarni, Borzoo Bonakdarpour, Ali Ebnenasir	Mechanical Verification of Automatic Synthesis of Fault-Tolerant Programs.	LOPSTR	2004	DBLP DOI BibTeX RDF	Addition of faulttolerance, Fault-tolerance, Program transformation, Theorem proving, Program synthesis, PVS, Mechanical verification
15	Diana Toma, Dominique Borrione, Ghiath Al Sammane	Combining Several Paradigms for Circuit Validation and Verification.	CASSIS	2004	DBLP DOI BibTeX RDF
15	Fairouz Kamareddine, Manuel Maarek, J. B. Wells	Flexible Encoding of Mathematics on the Computer.	MKM	2004	DBLP DOI BibTeX RDF
15	Claudio Sacerdoti Coen	Mathematical Libraries as Proof Assistant Environments.	MKM	2004	DBLP DOI BibTeX RDF
15	Lars-Åke Fredlund, Dilian Gurov, Thomas Noll 0001, Mads Dam, Thomas Arts, Gennady Chugunov	A verification tool for ERLANG.	Int. J. Softw. Tools Technol. Transf.	2003	DBLP DOI BibTeX RDF	Formal methods, Theorem proving, Software verification
15	Jens Busch, Wolfgang Banzhaf	How to Program Artificial Chemistries.	ECAL	2003	DBLP DOI BibTeX RDF
15	Marcelo F. Frias, Carlos López Pombo, Gabriel Baum, Nazareno Aguirre, T. S. E. Maibaum	Taking Alloy to the Movies.	FME	2003	DBLP DOI BibTeX RDF
15	Francisco-Jesús Martín-Mateos, José-Antonio Alonso, María-José Hidalgo, José-Luis Ruiz-Reina	Formal Verification of Molecular Computational Models in ACL2: A Case Study.	CAEPIA	2003	DBLP DOI BibTeX RDF
15	Warren A. Hunt Jr., Robert Bellarmine Krug, J Strother Moore	Linear and Nonlinear Arithmetic in ACL2.	CHARME	2003	DBLP DOI BibTeX RDF
15	Ralph D. Jeffords, Constance L. Heitmeyer	A strategy for efficiently verifying requirements.	ESEC / SIGSOFT FSE	2003	DBLP DOI BibTeX RDF	model checking, formal methods, software tools, invariants, requirements specification, compositional verification
15	Jinghai Rao, Xiaomeng Su	Toward the Composition of Semantic Web Services.	GCC (2)	2003	DBLP DOI BibTeX RDF
15	Stefan Blom, Jaco van de Pol	State Space Reduction by Proving Confluence.	CAV	2002	DBLP DOI BibTeX RDF	on-the-fly state space reduction, symbolic transformation, &#55CRL tool set, theorem proving, Labeled transition systems, partial order reduction, confluence, branching bisimulation
15	Aleksey Nogin, Jason Hickey	Sequent Schema for Derived Rules.	TPHOLs	2002	DBLP DOI BibTeX RDF
15	Michael W. Whalen, Johann Schumann, Bernd Fischer 0002	Synthesizing Certified Code.	FME	2002	DBLP DOI BibTeX RDF	automatic program synthesis, code certification, program verification, automated theorem proving, proof-carrying code
15	Michael Backes 0001, Christian Jacobi 0002, Birgit Pfitzmann	Deriving Cryptographically Sound Implementations Using Composition and Formally Verified Bisimulation.	FME	2002	DBLP DOI BibTeX RDF	security, cryptography, formal verification, PVS, simulatability
15	Ashish Tiwari 0001, Gaurav Khanna 0001	Series of Abstractions for Hybrid Automata.	HSCC	2002	DBLP DOI BibTeX RDF
15	Luís Cruz-Filipe	A Constructive Formalization of the Fundamental Theorem of Calculus.	TYPES	2002	DBLP DOI BibTeX RDF
15	Hans de Nivelle	Extraction of Proofs from the Clausal Normal Form Transformation.	CSL	2002	DBLP DOI BibTeX RDF
15	Marianne Brown	Selecting Semantics for Use with Semantic Pruning of Linear Deductions.	Australian Joint Conference on Artificial Intelligence	2002	DBLP DOI BibTeX RDF
15	Jeremy E. Dawson, Rajeev Goré	Machine-Checking the Timed Interval Calculus.	Australian Joint Conference on Artificial Intelligence	2002	DBLP DOI BibTeX RDF	Reasoning about time, theorem proving, automated reasoning
15	Christoph Kern, Tarik Ono-Tesfaye, Mark R. Greenstreet	A light-weight framework for hardware verification.	Int. J. Softw. Tools Technol. Transf.	2001	DBLP DOI BibTeX RDF	Refinement, Theorem-proving, Timing verification, Switch-level models, SRT division
15	Giampaolo Bella, Lawrence C. Paulson	Mechanical Proofs about a Non-repudiation Protocol.	TPHOLs	2001	DBLP DOI BibTeX RDF
15	Klaus Schneider 0001	Embedding Imperative Synchronous Languages in Interactive Theorem Provers.	ACSD	2001	DBLP DOI BibTeX RDF
15	Uwe Waldmann	Superposition and Chaining for Totally Ordered Divisible Abelian Groups.	IJCAR	2001	DBLP DOI BibTeX RDF
15	Andrea Formisano 0001, Eugenio G. Omodeo, Marco Temperini	Instructing Equational Set-Reasoning with Otter.	IJCAR	2001	DBLP DOI BibTeX RDF	Set reasoning, map algebra, first-order theorem proving
15	Roope Kaivola, Mark D. Aagaard	Divider Circuit Verification with Model Checking and Theorem Proving.	TPHOLs	2000	DBLP DOI BibTeX RDF
15	Jens Schönherr, Bernd Straube	Automatic Equivalence Check of Circuit Descriptions at Clocked Algorithmic and Register Transfer Level.	DATE	2000	DBLP DOI BibTeX RDF
15	Marianne Brown, Geoff Sutcliffe	System Description: PTTP+GLiDes: Semantically Guided PTTP.	CADE	2000	DBLP DOI BibTeX RDF
15	Alexandre Riazanov, Andrei Voronkov	Partially Adaptive Code Trees.	JELIA	2000	DBLP DOI BibTeX RDF	term indexing, code trees, matching, automated theorem proving, subsumption
15	Florian Kammüller, Markus Wenzel 0001, Lawrence C. Paulson	Locales - A Sectioning Concept for Isabelle.	TPHOLs	1999	DBLP DOI BibTeX RDF
15	Nazanin Mansouri, Ranga Vemuri	Accounting for Various Register Allocation Schemes During Post-Synthesis Verification of RTL Designs.	DATE	1999	DBLP DOI BibTeX RDF
15	Xiaoping Jia, Sushant Sawant, Jiangyu Zhou, Sotiris Skevoulis	Detecting Null Pointer Violations in Java Programs.	COMPSAC	1999	DBLP DOI BibTeX RDF
15	Jacques D. Fleuriot, Lawrence C. Paulson	Proving Newton's Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle.	Automated Deduction in Geometry	1998	DBLP DOI BibTeX RDF
15	Matthew Wilding	A Machine-Checked Proof of the Optimality of a Real-Time Scheduling Policy.	CAV	1998	DBLP DOI BibTeX RDF
15	David A. Plaisted, Yunshan Zhu	Replacement Rules with Definition Detection.	FTP (LNCS Selection)	1998	DBLP DOI BibTeX RDF
15	Hajime Sawamura, Daisaku Asanuma	Mechanizing Relevant Logics with HOL.	TPHOLs	1998	DBLP DOI BibTeX RDF
15	Florian Kammüller	Modular Structures as Dependent Types in Isabelle.	TYPES	1998	DBLP DOI BibTeX RDF
15	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
15	Carsten Schürmann, Frank Pfenning	Automated Theorem Proving in a Simple Meta-Logic for LF.	CADE	1998	DBLP DOI BibTeX RDF
15	Andreas Wolf	p-SETHEO: Strategy Parallelism in Automated Theorem Proving.	TABLEAUX	1998	DBLP DOI BibTeX RDF
15	Andreas Wolf	Strategy Selection for Automated Theorem Proving.	AIMSA	1998	DBLP DOI BibTeX RDF
15	Martin Simons 0001	Proof Presentation for Isabelle.	TPHOLs	1997	DBLP DOI BibTeX RDF
15	Sten Agerholm, Jacob Frost	Towards an Integrated CASE and Theorem Proving Tool for VDM-SL.	FME	1997	DBLP DOI BibTeX RDF
15	Bernd Fischer 0002, Johann Schumann	SETHEO Goes Software Engineering: Application of ATP to Software Reuse.	CADE	1997	DBLP DOI BibTeX RDF
15	Susanne Graf, Hassen Saïdi	Verifying Invariants Using theorem Proving.	CAV	1996	DBLP DOI BibTeX RDF
15	Edmund M. Clarke, Steven M. German, Xudong Zhao 0005	Verifying the SRT Division Algorithm Using Theorem Proving Techniques.	CAV	1996	DBLP DOI BibTeX RDF
15	Leopoldo E. Bertossi, Javier Pinto, Pablo Sáez, Deepak Kapur, Mahadevan Subramaniam	Automating Proofs of Integrity Constraints in Situation Calculus.	ISMIS	1996	DBLP DOI BibTeX RDF
15	Tanel Tammet, Jan M. Smith	Optimized Encodings of Fragments of Type Theory in First Order Logic.	TYPES	1995	DBLP DOI BibTeX RDF
15	Holger Busch	First-Order Automation for Higher-Order-Logic Theorem Proving.	TPHOLs	1994	DBLP DOI BibTeX RDF
15	I. S. W. B. Prasetya	Towards a Mechanically Supported and Compositional Calculus to Design Destributed Algorithms.	TPHOLs	1994	DBLP DOI BibTeX RDF
15	Laurent Vigneron	Associative-Commutative Deduction with Constraints.	CADE	1994	DBLP DOI BibTeX RDF
15	Mark E. Stickel, Richard J. Waldinger, Michael R. Lowry, Thomas Pressburger, Ian Underwood	Deductive Composition of Astronomical Software from Subroutine Libraries.	CADE	1994	DBLP DOI BibTeX RDF
15	Manfred Broy, Ursula Hinkel, Tobias Nipkow, Christian Prehofer, Birgit Schieder	Interpreter Verification for a Functional Language.	FSTTCS	1994	DBLP DOI BibTeX RDF
15	Deepak Kapur, Mahadevan Subramaniam	Using Linear Arithmetic Procedure for Generating Induction Schemes.	FSTTCS	1994	DBLP DOI BibTeX RDF
15	Reiner Hähnle, Werner Kernig	Verification of Switch-Level Designs with Many-Valued Logic.	LPAR	1993	DBLP DOI BibTeX RDF
15	John Harrison 0001, Laurent Théry	Reasoning About the Reals: The Marriage of HOL and Maple.	LPAR	1993	DBLP DOI BibTeX RDF
15	Hardi Hungar	Combining Model Checking and Theorem Proving to Verify Parallel Processes.	CAV	1993	DBLP DOI BibTeX RDF
15	Robert P. Kurshan, Leslie Lamport	Verification of a Multiplier: 64 Bits and Beyond.	CAV	1993	DBLP DOI BibTeX RDF
15	I. S. W. B. Prasetya	Formalization of Variables Access Constraints to Support Compositionality of Liveness Properties.	HUG	1993	DBLP DOI BibTeX RDF
15	Ricardo Caferra, Michel Herment	GLEFATINF: A Graphic Framework for Combining Theorem Provers and Editing Proofs for Different Logics.	DISCO	1993	DBLP DOI BibTeX RDF	Graphic Proof Presentation, Proof Edition, Logical Frameworks
15	Dominique Borrione, Laurence V. Pierre, Ashraf M. Salem	Formal Verification of VHDL Descriptions in the Prevail Environment.	IEEE Des. Test Comput.	1992	DBLP DOI BibTeX RDF
15	Geoffrey D. Alexander, David A. Plaisted	Proving Equality Theorems with Hyper-Linking.	CADE	1992	DBLP DOI BibTeX RDF
15	David A. Randell, Anthony G. Cohn 0001, Zhan Cui	Computing Transivity Tables: A Challenge For Automated Theorem Provers.	CADE	1992	DBLP DOI BibTeX RDF
15	Dave Barker-Plummer, Sidney C. Bailin, Andrew S. Merrill	&: Automated Natural Deduction.	CADE	1992	DBLP DOI BibTeX RDF
15	Paul Loewenstein, David L. Dill	Verification of a Multiprocessor Cache Protocol Using Simulation Relations and Higher-Order Logic.	CAV	1990	DBLP DOI BibTeX RDF
15	Amy P. Felty, Dale Miller 0001	Encoding a Dependent-Type Lambda-Calculus in a Logic Programming Language.	CADE	1990	DBLP DOI BibTeX RDF