Search results for "theorem-prover"

Hits ?▲	Authors	Title	Venue	Year	Link
23	Alessandro Coglio, Shilpi Goel	Adding 32-bit Mode to the ACL2 Model of the x86 ISA.	ACL2	2018	DBLP DOI BibTeX RDF
23	Matt Kaufmann	DefunT: A Tool for Automating Termination Proofs by Using the Community Books (Extended Abstract).	ACL2	2018	DBLP DOI BibTeX RDF
23	Carl Kwan, Mark R. Greenstreet	Convex Functions in ACL2(r).	ACL2	2018	DBLP DOI BibTeX RDF
23	Sol Swords	Hint Orchestration Using ACL2's Simplifier.	ACL2	2018	DBLP DOI BibTeX RDF
23	Yan Peng, Mark R. Greenstreet	Smtlink 2.0.	ACL2	2018	DBLP DOI BibTeX RDF
23	Sol Swords	Incremental SAT Library Integration Using Abstract Stobjs.	ACL2	2018	DBLP DOI BibTeX RDF
23	David S. Hardin, Konrad Slind	Using ACL2 in the Design of Efficient, Verifiable Data Structures for High-Assurance Systems.	ACL2	2018	DBLP DOI BibTeX RDF
23	Ruben Gamboa, John R. Cowles	The Fundamental Theorem of Algebra in ACL2.	ACL2	2018	DBLP DOI BibTeX RDF
23	Alessandro Coglio	A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java.	ACL2	2018	DBLP DOI BibTeX RDF
23	Lasha Abzianidze	LangPro: Natural Language Theorem Prover.	CoRR	2017	DBLP BibTeX RDF
23	Anna Slobodová, Warren A. Hunt Jr. (eds.)	Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, May 22-23, 2017.	ACL2	2017	DBLP BibTeX RDF
23	Giles Reger, Martin Suda 0001, Andrei Voronkov	Testing a Saturation-Based Theorem Prover: Experiences and Challenges (Extended Version).	CoRR	2017	DBLP BibTeX RDF
23	Daniyar Itegulov, John Slaney, Bruno Woltzenlogel Paleo	Scavenger 0.1: A Theorem Prover Based on Conflict Resolution.	CoRR	2017	DBLP BibTeX RDF
23	Mario Frank 0002, Christoph Kreitz	A Theorem Prover for Scientific and Educational Purposes.	ThEdu@CADE	2017	DBLP DOI BibTeX RDF
23	M. Ganesalingam, W. T. Gowers 0001	A Fully Automatic Theorem Prover with Human-Style Output.	J. Autom. Reason.	2017	DBLP DOI BibTeX RDF
23	Felicidad Aguado, Pablo Ascariz, Pedro Cabalar, Gilberto Pérez 0001, Concepción Vidal	Verification for ASP denotational semantics: A case study using the PVS theorem prover.	Log. J. IGPL	2017	DBLP DOI BibTeX RDF
23	Vladimir Pavlov, Vadim Pak	WhaleProver: First-Order Intuitionistic Theorem Prover Based on the Inverse Method.	Ershov Informatics Conference	2017	DBLP DOI BibTeX RDF
23	Kenneth Roe, Scott F. Smith 0001	Using the coq theorem prover to verify complex data structure invariants.	MEMOCODE	2017	DBLP DOI BibTeX RDF
23	Daniyar Itegulov, John Slaney, Bruno Woltzenlogel Paleo	Scavenger 0.1: A Theorem Prover Based on Conflict Resolution.	CADE	2017	DBLP DOI BibTeX RDF
23	Jian Zhong, Feng Cao, Guanfeng Wu, Yang Xu 0001, Jun Liu 0001	Multi-clause synergized contradiction separation based first-order theorem prover - MC-SCS.	ISKE	2017	DBLP DOI BibTeX RDF
23	Giles Reger, Martin Suda 0001, Andrei Voronkov	Testing a Saturation-Based Theorem Prover: Experiences and Challenges.	TAP@STAF	2017	DBLP DOI BibTeX RDF
23	Lasha Abzianidze	LangPro: Natural Language Theorem Prover.	EMNLP (System Demonstrations)	2017	DBLP DOI BibTeX RDF
23	Zhenwei Ma, Gang Chen	Formal Derivation and Verification of Coordinate Transformations in Theorem Prover Coq.	DSA	2017	DBLP DOI BibTeX RDF
23	Rob Sumners	Proof Reduction of Fair Stuttering Refinement of Asynchronous Systems and Applications.	ACL2	2017	DBLP DOI BibTeX RDF
23	John R. Cowles, Ruben Gamboa	The Cayley-Dickson Construction in ACL2.	ACL2	2017	DBLP DOI BibTeX RDF
23	Sol Swords	Term-Level Reasoning in Support of Bit-blasting.	ACL2	2017	DBLP DOI BibTeX RDF
23	Matt Kaufmann, Sol Swords	Meta-extract: Using Existing Facts in Meta-reasoning.	ACL2	2017	DBLP DOI BibTeX RDF
23	David M. Russinoff	A Computationally Surveyable Proof of the Group Properties of an Elliptic Curve.	ACL2	2017	DBLP DOI BibTeX RDF
23	Alessandro Coglio, Matt Kaufmann, Eric Whitman Smith	A Versatile, Sound Tool for Simplifying Definitions.	ACL2	2017	DBLP DOI BibTeX RDF
23	Shilpi Goel	The x86isa Books: Features, Usage, and Future Plans.	ACL2	2017	DBLP DOI BibTeX RDF
23	Richard Moot	The Grail theorem prover: Type theory for syntax and semantics.	CoRR	2016	DBLP BibTeX RDF
23	Cornelius Diekmann, Andreas Korsten, Georg Carle	Demonstrating topoS: Theorem-Prover-Based Synthesis of Secure Network Configurations.	CoRR	2016	DBLP BibTeX RDF
23	Daniel Whalen	Holophrasm: a neural Automated Theorem Prover for higher-order logic.	CoRR	2016	DBLP BibTeX RDF
23	Tao Liu, Yangjia Li, Shuling Wang, Mingsheng Ying, Naijun Zhan	A Theorem Prover for Quantum Hoare Logic and Its Applications.	CoRR	2016	DBLP BibTeX RDF
23	Jakob von Raumer	Formalizing Double Groupoids and Cross Modules in the Lean Theorem Prover.	ICMS	2016	DBLP DOI BibTeX RDF
23	Huazhen Xu, Zhen You, Jinyun Xue	Automatic verification of non-recursive algorithm of Hanoi Tower by using Isabelle Theorem Prover.	SNPD	2016	DBLP DOI BibTeX RDF
23	Leonardo de Moura 0001	Formalizing Mathematics using the Lean Theorem Prover.	ISAIM	2016	DBLP BibTeX RDF
23	Niki Vazou	Liquid Haskell: Haskell as a Theorem Prover.		2016	RDF
23	José Alberto Maestro-Prieto, Arancha Simón Hurtado	Adding a graphical output to a theorem prover: Results of a comparison of the acceptance from a teaching point of view.	Comput. Appl. Eng. Educ.	2015	DBLP DOI BibTeX RDF
23	Matt Kaufmann, David L. Rager (eds.)	Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015.	ACL2	2015	DBLP DOI BibTeX RDF
23	Jared Davis, Magnus O. Myreen	The Reflective Milawa Theorem Prover is Sound (Down to the Machine Code that Runs it).	J. Autom. Reason.	2015	DBLP DOI BibTeX RDF
23	Eric Smith, Alessandro Coglio	Android Platform Modeling and Android App Verification in the ACL2 Theorem Prover.	VSTTE	2015	DBLP DOI BibTeX RDF
23	Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer	The Lean Theorem Prover (System Description).	CADE	2015	DBLP DOI BibTeX RDF
23	Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp, André Platzer	KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems.	CADE	2015	DBLP DOI BibTeX RDF
23	Peter Baumgartner 0001, Joshua Bax, Uwe Waldmann	Beagle - A Hierarchic Superposition Theorem Prover.	CADE	2015	DBLP DOI BibTeX RDF
23	Cornelius Diekmann, Andreas Korsten, Georg Carle	Demonstrating topoS: Theorem-prover-based synthesis of secure network configurations.	CNSM	2015	DBLP DOI BibTeX RDF
23	Noriaki Yoshiura	Implementation of Theorem Prover of Relevant Logic.	IEA/AIE	2015	DBLP DOI BibTeX RDF
23	Laura Giordano 0001, Valentina Gliozzi, Nicola Olivetti, Gian Luca Pozzato, Luca Violanti	DysToPic: a Multi-Engine Theorem Prover for Preferential Description Logics.	Description Logics	2015	DBLP BibTeX RDF
23	Laura Giordano 0001, Valentina Gliozzi, Nicola Olivetti, Gian Luca Pozzato, Luca Violanti	A Multi-engine Theorem Prover for a Description Logic of Typicality.	AI*IA	2015	DBLP DOI BibTeX RDF
23	Nourah Shenaiber	Analyzing the selection of the herbrand base process for building a Smart Semantic Tree Theorem Prover.		2015	RDF
23	David S. Hardin	Reasoning About LLVM Code Using Codewalker.	ACL2	2015	DBLP DOI BibTeX RDF
23	John R. Cowles, Ruben Gamboa	Perfect Numbers in ACL2.	ACL2	2015	DBLP DOI BibTeX RDF
23	J Strother Moore	Stateman: Using Metafunctions to Manage Large Terms Representing Machine States.	ACL2	2015	DBLP DOI BibTeX RDF
23	Cuong K. Chau, Matt Kaufmann, Warren A. Hunt Jr.	Fourier Series Formalization in ACL2(r).	ACL2	2015	DBLP DOI BibTeX RDF
23	Mitesh Jain, Panagiotis Manolios	Proving Skipping Refinement with ACL2s.	ACL2	2015	DBLP DOI BibTeX RDF
23	Sol Swords, Jared Davis	Fix Your Types.	ACL2	2015	DBLP DOI BibTeX RDF
23	Alessandro Coglio	Second-Order Functions and Theorems in ACL2.	ACL2	2015	DBLP DOI BibTeX RDF
23	Yan Peng, Mark R. Greenstreet	Extending ACL2 with SMT Solvers.	ACL2	2015	DBLP DOI BibTeX RDF
23	Freek Verbeek, Julien Schmaltz (eds.)	Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014.	ACL2	2014	DBLP DOI BibTeX RDF
23	Sitar Kortik, Uluc Saranli	Linear planning logic: An efficient language and theorem prover for robotic task planning.	ICRA	2014	DBLP DOI BibTeX RDF
23	Rajeev Goré, Jimmy Thomson 0001, Jesse Wu	A History-Based Theorem Prover for Intuitionistic Propositional Logic Using Global Caching: IntHistGC System Description.	IJCAR	2014	DBLP DOI BibTeX RDF
23	Jasmin Christian Blanchette	My Life with an Automatic Theorem Prover.	Vampire Workshop	2014	DBLP DOI BibTeX RDF
23	Dipak L. Chaudhari, Om P. Damani	Automated Theorem Prover Assisted Program Calculations.	IFM	2014	DBLP DOI BibTeX RDF
23	Magnus O. Myreen, Jared Davis	The Reflective Milawa Theorem Prover Is Sound - (Down to the Machine Code That Runs It).	ITP	2014	DBLP DOI BibTeX RDF
23	Disha Puri, Sandip Ray, Kecheng Hao, Fei Xie	Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis.	ACL2	2014	DBLP DOI BibTeX RDF
23	Matt Kaufmann, J Strother Moore	Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4.	ACL2	2014	DBLP DOI BibTeX RDF
23	Jared Davis, Matt Kaufmann	Industrial-Strength Documentation for ACL2.	ACL2	2014	DBLP DOI BibTeX RDF
23	Sebastiaan J. C. Joosten, Cezary Kaliszyk, Josef Urban	Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems.	ACL2	2014	DBLP DOI BibTeX RDF
23	Harsh Raju Chamarthi, Peter C. Dillinger, Panagiotis Manolios	Data Definitions in the ACL2 Sedan.	ACL2	2014	DBLP DOI BibTeX RDF
23	Jónathan Heras, Ekaterina Komendantskaya	ACL2(ml): Machine-Learning for ACL2.	ACL2	2014	DBLP DOI BibTeX RDF
23	Ruben Gamboa, John R. Cowles	Formal Verification of Medina's Sequence of Polynomials for Approximating Arctangent.	ACL2	2014	DBLP DOI BibTeX RDF
23	Benjamin Selfridge, Eric Smith	Polymorphic Types in ACL2.	ACL2	2014	DBLP DOI BibTeX RDF
23	John R. Cowles, Ruben Gamboa	Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis.	ACL2	2014	DBLP DOI BibTeX RDF
23	Benjamin Selfridge	An ACL2 Mechanization of an Axiomatic Framework for Weak Memory.	ACL2	2014	DBLP DOI BibTeX RDF
23	John W. O'Leary, David M. Russinoff	Modeling Algorithms in SystemC and ACL2.	ACL2	2014	DBLP DOI BibTeX RDF
23	David S. Hardin, Jennifer A. Davis, David A. Greve, Jedidiah R. McClurg	Development of a Translator from LLVM to ACL2.	ACL2	2014	DBLP DOI BibTeX RDF
23	Tom Melham, Raphael Cohn, Ian Childs	On the Semantics of ReFLect as a Basis for a Reflective Theorem Prover.	CoRR	2013	DBLP BibTeX RDF
23	Ruben Gamboa, Jared Davis (eds.)	Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2013, Laramie, Wyoming, USA, May 30-31, 2013.	ACL2	2013	DBLP DOI BibTeX RDF
23	James P. Bridge, Lawrence C. Paulson	Case Splitting in an Automatic Theorem Prover for Real-Valued Special Functions.	J. Autom. Reason.	2013	DBLP DOI BibTeX RDF
23	Achim D. Brucker, Burkhart Wolff	On theorem prover-based testing.	Formal Aspects Comput.	2013	DBLP DOI BibTeX RDF
23	Bo Meng, Wei Huang, Zimao Li	Automated Proof of Resistance of Denial of Service Attacks Using Event with Theorem Prover.	J. Comput.	2013	DBLP BibTeX RDF
23	Jonghyun Park, Jeongbong Seo, Sungwoo Park	A theorem prover for Boolean BI.	POPL	2013	DBLP DOI BibTeX RDF
23	David L. Rager, Warren A. Hunt Jr., Matt Kaufmann	A Parallelized Theorem Prover for a Logic with Parallel Execution.	ITP	2013	DBLP DOI BibTeX RDF
23	Daniel Gâinâ, Min Zhang 0002, Yuki Chiba, Yasuhito Arimoto	Constructor-Based Inductive Theorem Prover.	CALCO	2013	DBLP DOI BibTeX RDF
23	Laura Giordano 0001, Valentina Gliozzi, Adam Jalal, Nicola Olivetti, Gian Luca Pozzato	PreDeLo 1.0: A Theorem Prover for Preferential Description Logics.	AI*IA	2013	DBLP DOI BibTeX RDF
23	Jared Davis, Sol Swords	Verified AIG Algorithms in ACL2	ACL2	2013	DBLP DOI BibTeX RDF
23	Matt Kaufmann, J Strother Moore	Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1	ACL2	2013	DBLP DOI BibTeX RDF
23	Bernard van Gastel, Julien Schmaltz	A formalisation of XMAS	ACL2	2013	DBLP DOI BibTeX RDF
23	Caleb Eggensperger	Proof Pad: A New Development Environment for ACL2	ACL2	2013	DBLP DOI BibTeX RDF
23	David A. Greve, Konrad Slind	A Step-Indexing Approach to Partial Functions	ACL2	2013	DBLP DOI BibTeX RDF
23	Lucas Helms, Ruben Gamboa	An Interpreter for Quantum Circuits	ACL2	2013	DBLP DOI BibTeX RDF
23	Shilpi Goel, Warren A. Hunt Jr., Matt Kaufmann	Abstract Stobjs and Their Application to ISA Modeling	ACL2	2013	DBLP DOI BibTeX RDF
23	Sebastiaan J. C. Joosten, Bernard van Gastel, Julien Schmaltz	A Macro for Reusing Abstract Functions and Theorems	ACL2	2013	DBLP DOI BibTeX RDF
23	David S. Hardin, Samuel S. Hardin	ACL2 Meets the GPU: Formalizing a CUDA-based Parallelizable All-Pairs Shortest Path Algorithm in ACL2	ACL2	2013	DBLP DOI BibTeX RDF
23	Freek Verbeek, Julien Schmaltz	Verification of Building Blocks for Asynchronous Circuits	ACL2	2013	DBLP DOI BibTeX RDF
23	Ferruccio Guidi	Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover.	J. Formaliz. Reason.	2012	DBLP DOI BibTeX RDF
23	Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi	Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover.	J. Autom. Reason.	2012	DBLP DOI BibTeX RDF
23	Md Zahidul Islam 0001, Ahmed Shah Mashiyat, Kashif Nizam Khan, S. M. Masud Karim	A Tableau Based Automated Theorem Prover Using High Performance Computing.	J. Comput.	2012	DBLP BibTeX RDF
23	J Strother Moore	Meta-level features in an industrial-strength theorem prover.	POPL	2012	DBLP DOI BibTeX RDF
23	James Brotherston, Nikos Gorogiannis, Rasmus Lerchedahl Petersen	A Generic Cyclic Theorem Prover.	APLAS	2012	DBLP DOI BibTeX RDF