Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
23 | Alessandro Coglio, Shilpi Goel |
Adding 32-bit Mode to the ACL2 Model of the x86 ISA. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018., pp. 77-94, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
23 | Matt Kaufmann |
DefunT: A Tool for Automating Termination Proofs by Using the Community Books (Extended Abstract). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018., pp. 161-163, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
23 | Carl Kwan, Mark R. Greenstreet |
Convex Functions in ACL2(r). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018., pp. 128-142, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
23 | Sol Swords |
Hint Orchestration Using ACL2's Simplifier. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018., pp. 164-171, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
23 | Yan Peng, Mark R. Greenstreet |
Smtlink 2.0. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018., pp. 143-160, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
23 | Sol Swords |
Incremental SAT Library Integration Using Abstract Stobjs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018., pp. 47-60, 2018. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018., pp. 61-76, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
23 | Ruben Gamboa, John R. Cowles |
The Fundamental Theorem of Algebra in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018., pp. 98-110, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
23 | Alessandro Coglio |
A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018., pp. 1-17, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
23 | Lasha Abzianidze |
LangPro: Natural Language Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1708.09417, 2017. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP BibTeX RDF |
|
23 | Giles Reger, Martin Suda 0001, Andrei Voronkov |
Testing a Saturation-Based Theorem Prover: Experiences and Challenges (Extended Version). ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1704.03391, 2017. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP BibTeX RDF |
|
23 | Daniyar Itegulov, John Slaney, Bruno Woltzenlogel Paleo |
Scavenger 0.1: A Theorem Prover Based on Conflict Resolution. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1704.03275, 2017. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP BibTeX RDF |
|
23 | Mario Frank 0002, Christoph Kreitz |
A Theorem Prover for Scientific and Educational Purposes. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ThEdu@CADE ![In: Proceedings 6th International Workshop on Theorem proving components for Educational software, ThEdu@CADE 2017, Gothenburg, Sweden, 6 Aug 2017., pp. 59-69, 2017. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
23 | M. Ganesalingam, W. T. Gowers 0001 |
A Fully Automatic Theorem Prover with Human-Style Output. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 58(2), pp. 253-291, 2017. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Log. J. IGPL ![In: Log. J. IGPL 25(2), pp. 195-213, 2017. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
23 | Vladimir Pavlov, Vadim Pak |
WhaleProver: First-Order Intuitionistic Theorem Prover Based on the Inverse Method. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Ershov Informatics Conference ![In: Perspectives of System Informatics - 11th International Andrei P. Ershov Informatics Conference, PSI 2017, Moscow, Russia, June 27-29, 2017, Revised Selected Papers, pp. 322-336, 2017, Springer, 978-3-319-74312-7. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
23 | Kenneth Roe, Scott F. Smith 0001 |
Using the coq theorem prover to verify complex data structure invariants. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MEMOCODE ![In: Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2017, Vienna, Austria, September 29 - October 02, 2017, pp. 118-121, 2017, ACM, 978-1-4503-5093-8. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
23 | Daniyar Itegulov, John Slaney, Bruno Woltzenlogel Paleo |
Scavenger 0.1: A Theorem Prover Based on Conflict Resolution. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, pp. 344-356, 2017, Springer, 978-3-319-63045-8. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISKE ![In: 12th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2017, Nanjing, China, November 24-26, 2017, pp. 1-6, 2017, IEEE, 978-1-5386-1829-5. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
23 | Giles Reger, Martin Suda 0001, Andrei Voronkov |
Testing a Saturation-Based Theorem Prover: Experiences and Challenges. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TAP@STAF ![In: Tests and Proofs - 11th International Conference, TAP@STAF 2017, Marburg, Germany, July 19-20, 2017, Proceedings, pp. 152-161, 2017, Springer, 978-3-319-61466-3. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
23 | Lasha Abzianidze |
LangPro: Natural Language Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
EMNLP (System Demonstrations) ![In: Proceedings of the 2017 Conference on Empirical Methods in Natural Language Processing, EMNLP 2017, Copenhagen, Denmark, September 9-11, 2017 - System Demonstrations, pp. 115-120, 2017, Association for Computational Linguistics, 978-1-945626-97-5. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
23 | Zhenwei Ma, Gang Chen |
Formal Derivation and Verification of Coordinate Transformations in Theorem Prover Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
DSA ![In: International Conference on Dependable Systems and Their Applications, DSA 2017, Beijing, China, October 31 - November 2, 2017, pp. 127-136, 2017, IEEE, 978-1-5386-3690-9. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
23 | Rob Sumners |
Proof Reduction of Fair Stuttering Refinement of Asynchronous Systems and Applications. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, May 22-23, 2017., pp. 78-94, 2017. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
23 | John R. Cowles, Ruben Gamboa |
The Cayley-Dickson Construction in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, May 22-23, 2017., pp. 18-29, 2017. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
23 | Sol Swords |
Term-Level Reasoning in Support of Bit-blasting. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, May 22-23, 2017., pp. 95-111, 2017. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
23 | Matt Kaufmann, Sol Swords |
Meta-extract: Using Existing Facts in Meta-reasoning. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, May 22-23, 2017., pp. 47-60, 2017. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
23 | David M. Russinoff |
A Computationally Surveyable Proof of the Group Properties of an Elliptic Curve. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, May 22-23, 2017., pp. 30-46, 2017. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
23 | Alessandro Coglio, Matt Kaufmann, Eric Whitman Smith |
A Versatile, Sound Tool for Simplifying Definitions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, May 22-23, 2017., pp. 61-77, 2017. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
23 | Shilpi Goel |
The x86isa Books: Features, Usage, and Future Plans. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, May 22-23, 2017., pp. 1-17, 2017. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
23 | Richard Moot |
The Grail theorem prover: Type theory for syntax and semantics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1602.00812, 2016. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP BibTeX RDF |
|
23 | Cornelius Diekmann, Andreas Korsten, Georg Carle |
Demonstrating topoS: Theorem-Prover-Based Synthesis of Secure Network Configurations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1604.00273, 2016. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP BibTeX RDF |
|
23 | Daniel Whalen |
Holophrasm: a neural Automated Theorem Prover for higher-order logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1608.02644, 2016. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1601.03835, 2016. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP BibTeX RDF |
|
23 | Jakob von Raumer |
Formalizing Double Groupoids and Cross Modules in the Lean Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICMS ![In: Mathematical Software - ICMS 2016 - 5th International Conference, Berlin, Germany, July 11-14, 2016, Proceedings, pp. 28-33, 2016, Springer, 978-3-319-42431-6. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SNPD ![In: 17th IEEE/ACIS International Conference on Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computing, SNPD 2016, Shanghai, China, May 30 - June 1, 2016, pp. 13-18, 2016, IEEE Computer Society, 978-1-5090-2239-7. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
23 | Leonardo de Moura 0001 |
Formalizing Mathematics using the Lean Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISAIM ![In: International Symposium on Artificial Intelligence and Mathematics, ISAIM 2016, Fort Lauderdale, Florida, USA, January 4-6, 2016., 2016. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP BibTeX RDF |
|
23 | Niki Vazou |
Liquid Haskell: Haskell as a Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Comput. Appl. Eng. Educ. ![In: Comput. Appl. Eng. Educ. 23(6), pp. 837-845, 2015. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![The full citation details ...](Pics/full.jpeg) |
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). ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 55(2), pp. 117-183, 2015. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
23 | Eric Smith, Alessandro Coglio |
Android Platform Modeling and Android App Verification in the ACL2 Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
VSTTE ![In: Verified Software: Theories, Tools, and Experiments - 7th International Conference, VSTTE 2015, San Francisco, CA, USA, July 18-19, 2015. Revised Selected Papers, pp. 183-201, 2015, Springer, 978-3-319-29612-8. The full citation details ...](Pics/full.jpeg) |
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). ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, pp. 378-388, 2015, Springer, 978-3-319-21400-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, pp. 527-538, 2015, Springer, 978-3-319-21400-9. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
23 | Peter Baumgartner 0001, Joshua Bax, Uwe Waldmann |
Beagle - A Hierarchic Superposition Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, pp. 367-377, 2015, Springer, 978-3-319-21400-9. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
23 | Cornelius Diekmann, Andreas Korsten, Georg Carle |
Demonstrating topoS: Theorem-prover-based synthesis of secure network configurations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CNSM ![In: 11th International Conference on Network and Service Management, CNSM 2015, Barcelona, Spain, November 9-13, 2015, pp. 366-371, 2015, IEEE Computer Society, 978-3-9018-8277-7. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
23 | Noriaki Yoshiura |
Implementation of Theorem Prover of Relevant Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEA/AIE ![In: Current Approaches in Applied Artificial Intelligence - 28th International Conference on Industrial, Engineering and Other Applications of Applied Intelligent Systems, IEA/AIE 2015, Seoul, South Korea, June 10-12, 2015, Proceedings, pp. 13-22, 2015, Springer, 978-3-319-19065-5. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Description Logics ![In: Proceedings of the 28th International Workshop on Description Logics, Athens,Greece, June 7-10, 2015., 2015, CEUR-WS.org. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AI*IA ![In: AI*IA 2015, Advances in Artificial Intelligence - XIVth International Conference of the Italian Association for Artificial Intelligence, Ferrara, Italy, September 23-25, 2015, Proceedings, pp. 164-178, 2015, Springer, 978-3-319-24308-5. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
23 | Nourah Shenaiber |
Analyzing the selection of the herbrand base process for building a Smart Semantic Tree Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2015 |
RDF |
|
23 | David S. Hardin |
Reasoning About LLVM Code Using Codewalker. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015., pp. 79-92, 2015. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
23 | John R. Cowles, Ruben Gamboa |
Perfect Numbers in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015., pp. 53-59, 2015. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
23 | J Strother Moore |
Stateman: Using Metafunctions to Manage Large Terms Representing Machine States. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015., pp. 93-109, 2015. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
23 | Cuong K. Chau, Matt Kaufmann, Warren A. Hunt Jr. |
Fourier Series Formalization in ACL2(r). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015., pp. 35-51, 2015. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
23 | Mitesh Jain, Panagiotis Manolios |
Proving Skipping Refinement with ACL2s. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015., pp. 111-127, 2015. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
23 | Sol Swords, Jared Davis |
Fix Your Types. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015., pp. 3-16, 2015. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
23 | Alessandro Coglio |
Second-Order Functions and Theorems in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015., pp. 17-33, 2015. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
23 | Yan Peng, Mark R. Greenstreet |
Extending ACL2 with SMT Solvers. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015., pp. 61-77, 2015. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
23 | Sitar Kortik, Uluc Saranli |
Linear planning logic: An efficient language and theorem prover for robotic task planning. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICRA ![In: 2014 IEEE International Conference on Robotics and Automation, ICRA 2014, Hong Kong, China, May 31 - June 7, 2014, pp. 3764-3770, 2014, IEEE. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings, pp. 262-268, 2014, Springer, 978-3-319-08586-9. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
23 | Jasmin Christian Blanchette |
My Life with an Automatic Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Vampire Workshop ![In: Proceedings of the 1st and 2nd Vampire Workshops, Vampire@VSL 2014, Vienna, Austria, July 23, 2014 / Vampire@CADE 2015, Berlin, Germany, August 2, 2015, pp. 1-7, 2014, EasyChair. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
23 | Dipak L. Chaudhari, Om P. Damani |
Automated Theorem Prover Assisted Program Calculations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IFM ![In: Integrated Formal Methods - 11th International Conference, IFM 2014, Bertinoro, Italy, September 9-11, 2014, Proceedings, pp. 205-220, 2014, Springer, 978-3-319-10180-4. The full citation details ...](Pics/full.jpeg) |
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). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, pp. 421-436, 2014, Springer, 978-3-319-08969-0. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
23 | Disha Puri, Sandip Ray, Kecheng Hao, Fei Xie |
Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014., pp. 111-128, 2014. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
23 | Matt Kaufmann, J Strother Moore |
Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014., pp. 1-7, 2014. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
23 | Jared Davis, Matt Kaufmann |
Industrial-Strength Documentation for ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014., pp. 9-25, 2014. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014., pp. 77-85, 2014. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
23 | Harsh Raju Chamarthi, Peter C. Dillinger, Panagiotis Manolios |
Data Definitions in the ACL2 Sedan. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014., pp. 27-48, 2014. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
23 | Jónathan Heras, Ekaterina Komendantskaya |
ACL2(ml): Machine-Learning for ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014., pp. 61-75, 2014. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
23 | Ruben Gamboa, John R. Cowles |
Formal Verification of Medina's Sequence of Polynomials for Approximating Arctangent. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014., pp. 101-110, 2014. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
23 | Benjamin Selfridge, Eric Smith |
Polymorphic Types in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014., pp. 49-59, 2014. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
23 | John R. Cowles, Ruben Gamboa |
Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014., pp. 89-100, 2014. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
23 | Benjamin Selfridge |
An ACL2 Mechanization of an Axiomatic Framework for Weak Memory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014., pp. 129-144, 2014. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
23 | John W. O'Leary, David M. Russinoff |
Modeling Algorithms in SystemC and ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014., pp. 145-162, 2014. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 12-13th July 2014., pp. 163-177, 2014. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1309.5742, 2013. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
23 | James P. Bridge, Lawrence C. Paulson |
Case Splitting in an Automatic Theorem Prover for Real-Valued Special Functions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 50(1), pp. 99-117, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
23 | Achim D. Brucker, Burkhart Wolff |
On theorem prover-based testing. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 25(5), pp. 683-721, 2013. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Comput. ![In: J. Comput. 8(7), pp. 1728-1741, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP BibTeX RDF |
|
23 | Jonghyun Park, Jeongbong Seo, Sungwoo Park |
A theorem prover for Boolean BI. ![Search on Bibsonomy](Pics/bibsonomy.png) |
POPL ![In: The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, Rome, Italy - January 23 - 25, 2013, pp. 219-232, 2013, ACM, 978-1-4503-1832-7. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, pp. 435-450, 2013, Springer, 978-3-642-39633-5. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
23 | Daniel Gâinâ, Min Zhang 0002, Yuki Chiba, Yasuhito Arimoto |
Constructor-Based Inductive Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CALCO ![In: Algebra and Coalgebra in Computer Science - 5th International Conference, CALCO 2013, Warsaw, Poland, September 3-6, 2013. Proceedings, pp. 328-333, 2013, Springer, 978-3-642-40205-0. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AI*IA ![In: AI*IA 2013: Advances in Artificial Intelligence - XIIIth International Conference of the Italian Association for Artificial Intelligence, Turin, Italy, December 4-6, 2013. Proceedings, pp. 60-72, 2013, Springer, 978-3-319-03523-9. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
23 | Jared Davis, Sol Swords |
Verified AIG Algorithms in ACL2 ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2013, Laramie, Wyoming, USA, May 30-31, 2013., pp. 95-110, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
23 | Matt Kaufmann, J Strother Moore |
Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1 ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2013, Laramie, Wyoming, USA, May 30-31, 2013., pp. 5-12, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
23 | Bernard van Gastel, Julien Schmaltz |
A formalisation of XMAS ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2013, Laramie, Wyoming, USA, May 30-31, 2013., pp. 111-126, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
23 | Caleb Eggensperger |
Proof Pad: A New Development Environment for ACL2 ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2013, Laramie, Wyoming, USA, May 30-31, 2013., pp. 13-28, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
23 | David A. Greve, Konrad Slind |
A Step-Indexing Approach to Partial Functions ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2013, Laramie, Wyoming, USA, May 30-31, 2013., pp. 42-53, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
23 | Lucas Helms, Ruben Gamboa |
An Interpreter for Quantum Circuits ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2013, Laramie, Wyoming, USA, May 30-31, 2013., pp. 85-94, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
23 | Shilpi Goel, Warren A. Hunt Jr., Matt Kaufmann |
Abstract Stobjs and Their Application to ISA Modeling ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2013, Laramie, Wyoming, USA, May 30-31, 2013., pp. 54-69, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
23 | Sebastiaan J. C. Joosten, Bernard van Gastel, Julien Schmaltz |
A Macro for Reusing Abstract Functions and Theorems ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2013, Laramie, Wyoming, USA, May 30-31, 2013., pp. 29-41, 2013. The full citation details ...](Pics/full.jpeg) |
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 ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2013, Laramie, Wyoming, USA, May 30-31, 2013., pp. 127-142, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
23 | Freek Verbeek, Julien Schmaltz |
Verification of Building Blocks for Asynchronous Circuits ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2013, Laramie, Wyoming, USA, May 30-31, 2013., pp. 70-84, 2013. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
23 | Ferruccio Guidi |
Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Formaliz. Reason. ![In: J. Formaliz. Reason. 5(1), pp. 1-25, 2012. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 49(3), pp. 427-451, 2012. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Comput. ![In: J. Comput. 7(3), pp. 597-607, 2012. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP BibTeX RDF |
|
23 | J Strother Moore |
Meta-level features in an industrial-strength theorem prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
POPL ![In: Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, pp. 425-426, 2012, ACM, 978-1-4503-1083-3. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
23 | James Brotherston, Nikos Gorogiannis, Rasmus Lerchedahl Petersen |
A Generic Cyclic Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
APLAS ![In: Programming Languages and Systems - 10th Asian Symposium, APLAS 2012, Kyoto, Japan, December 11-13, 2012. Proceedings, pp. 350-367, 2012, Springer, 978-3-642-35181-5. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|