Search results for "ACL2"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
22	Inmaculada Medina-Bulo, Francisco Palomo-Lozano, José-Luis Ruiz-Reina	A verified Common Lisp implementation of Buchberger's algorithm in ACL2.	J. Symb. Comput.	2010	DBLP DOI BibTeX RDF
22	Matt Kaufmann, J Strother Moore	ACL2 and Its Applications to Digital System Verification.	Design and Verification of Microprocessor Systems for High-Assurance Applications	2010	DBLP DOI BibTeX RDF
22	Carl Eastlund, Matthias Felleisen	Hygienic Macros for ACL2.	Trends in Functional Programming	2010	DBLP DOI BibTeX RDF
22	Jónathan Heras, Vico Pascual, Julio Rubio 0001	Proving with ACL2 the Correctness of Simplicial Sets in the Kenzo System.	LOPSTR	2010	DBLP DOI BibTeX RDF
22	Matt Kaufmann, J Strother Moore, Sandip Ray, Erik Reeber	Integrating external deduction tools with ACL2.	J. Appl. Log.	2009	DBLP DOI BibTeX RDF
22	James Reynolds	An automatic proof-generating translation from higher-order to first-order logic : with applications to linking HOL4 and ACL2.		2009	RDF
22	Maissa Elleuch, Yassine Aydi, Mohamed Abid	Formal Specification of Delta MINs for MPSOC in the ACL2 Logic.	FDL	2008	DBLP DOI BibTeX RDF
22	Peter C. Dillinger, Panagiotis Manolios, Daron Vroon 0001, J Strother Moore	ACL2s: "The ACL2 Sedan".	UITP@FLoC	2006	DBLP DOI BibTeX RDF
22	Ruben Gamboa	ACL2.	The Seventeen Provers of the World	2006	DBLP DOI BibTeX RDF
22	J Strother Moore	On the Adoption of Formal Methods by Industry: The ACL2 Experience.	ICFEM	2004	DBLP DOI BibTeX RDF
22	José-Luis Ruiz-Reina, José-Antonio Alonso, María-José Hidalgo, Francisco-Jesús Martín-Mateos	Formal Proofs About Rewriting Using ACL2.	Ann. Math. Artif. Intell.	2002	DBLP DOI BibTeX RDF
22	Ruben Gamboa	The Correctness of the Fast Fourier Transform: A Structured Proof in ACL2.	Formal Methods Syst. Des.	2002	DBLP DOI BibTeX RDF
22	Ruben Gamboa, Matt Kaufmann	Nonstandard Analysis in ACL2.	J. Autom. Reason.	2001	DBLP DOI BibTeX RDF
22	Vanderlei Moraes Rodrigues, Dominique Borrione, Philippe Georgelin	Using the ACL2 Theorem Prover to Reason about VHDL Components.	RITA	2000	DBLP BibTeX RDF
22	Vanderlei Moraes Rodrigues, Dominique Borrione, Philippe Georgelin	An ACL2 Model of VHDL for Symbolic Simulation and Formal Verification.	SBCCI	2000	DBLP BibTeX RDF
22	Ruben Gamboa	Mechanically Verifying the Correctness of the Fast Fourier Transform in ACL2.	IPPS/SPDP Workshops	1998	DBLP DOI BibTeX RDF
22	Bishop Brock, Matt Kaufmann, J Strother Moore	ACL2 Theorems About Commercial Microprocessors.	FMCAD	1996	DBLP DOI BibTeX RDF
22	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
14	Panagiotis Manolios, Aaron Turon	All-Termination(T).	TACAS	2009	DBLP DOI BibTeX RDF
14	Tom van den Broek, Julien Schmaltz	Towards a formally verified network-on-chip.	FMCAD	2009	DBLP DOI BibTeX RDF
14	Jónathan Heras, Vico Pascual, Julio Rubio 0001	Using Open Mathematical Documents to Interface Computer Algebra and Proof Assistant Systems.	Calculemus/MKM	2009	DBLP DOI BibTeX RDF
14	Julien Schmaltz, Dominique Borrione	A functional formalization of on chip communications.	Formal Aspects Comput.	2008	DBLP DOI BibTeX RDF	Formal methods, Networks on chip, Automated theorem proving, Communication architectures
14	Dominique Borrione, Amr Helmy, Laurence Pierre, Julien Schmaltz	Executable formal specification and validation of NoC communication infrastructures.	SBCCI	2008	DBLP DOI BibTeX RDF	simulation, verification, theorem proving
14	David S. Hardin	Invited Tutorial: Considerations in the Design and Verification of Microprocessors for Safety-Critical and Security-Critical Applications.	FMCAD	2008	DBLP DOI BibTeX RDF
14	Warren A. Hunt Jr., Robert Bellarmine Krug, Sandip Ray, William D. Young	Mechanized Information Flow Analysis through Inductive Assertions.	FMCAD	2008	DBLP DOI BibTeX RDF
14	Bart Jacobs 0001, Sjaak Smetsers, Ronny Wichers Schreur	Code-carrying theories.	Formal Aspects Comput.	2007	DBLP DOI BibTeX RDF	Compression, Code generation, Functional languages, Unification, PVS, Proof assistants
14	Sandip Ray, Warren A. Hunt Jr.	Mechanized Certification of Secure Hardware Designs.	MTV	2007	DBLP DOI BibTeX RDF
14	Victor L. Winter, Jason Beranek, Fares Fraij, Steve Roach, Gregory L. Wickstrom	A transformational perspective into the core of an abstract class loader for the SSP.	ACM Trans. Embed. Comput. Syst.	2006	DBLP DOI BibTeX RDF	HATS, Strategic programming, higher-order rewriting, TL, SSP
14	John Matthews, J Strother Moore, Sandip Ray, Daron Vroon 0001	Verification Condition Generation Via Theorem Proving.	LPAR	2006	DBLP DOI BibTeX RDF
14	Panagiotis Manolios	Refinement and Theorem Proving.	SFM	2006	DBLP DOI BibTeX RDF
14	Yves Bertot, Laurent Théry	Dependent Types, Theorem Proving, and Applications for a Verifying Compiler.	VSTTE	2005	DBLP DOI BibTeX RDF
14	Alessandro Armando, Luca Compagna, Silvio Ranise	Rewriting and Decision Procedure Laboratory: Combining Rewriting, Satisfiability Checking, and Lemma Speculation.	Mechanizing Mathematical Reasoning	2005	DBLP DOI BibTeX RDF
14	Sandip Ray, Warren A. Hunt Jr.	Deductive Verification of Pipelined Machines Using First-Order Quantification.	CAV	2004	DBLP DOI BibTeX RDF
14	Ruben Gamboa, John R. Cowles	A Mechanical Proof of the Cook-Levin Theorem.	TPHOLs	2004	DBLP DOI BibTeX RDF
14	Tao Song, Calvin Ko, Jim Alves-Foss, Cui Zhang, Karl N. Levitt	Formal Reasoning About Intrusion Detection Systems.	RAID	2004	DBLP DOI BibTeX RDF	verification, formal method, Intrusion detection, security policy
14	Diana Toma, Dominique Borrione, Ghiath Al Sammane	Combining Several Paradigms for Circuit Validation and Verification.	CASSIS	2004	DBLP DOI BibTeX RDF
14	Jonathan Ford, Natarajan Shankar	Formal Verification of a Combination Decision Procedure.	CADE	2002	DBLP DOI BibTeX RDF
14	Silvio Ranise	Combining Generic and Domain Specific Reasoning by Using Contexts.	AISC	2002	DBLP DOI BibTeX RDF
14	Jean-Christophe Filliâtre, Sam Owre, Harald Rueß, Natarajan Shankar	ICS: Integrated Canonizer and Solver.	CAV	2001	DBLP DOI BibTeX RDF
14	Inmaculada Medina-Bulo, Francisco Palomo-Lozano, José A. Alonso-Jiménez	A Certified Polynomial-Based Decision Procedure for Propositional Logic.	TPHOLs	2001	DBLP DOI BibTeX RDF
14	Alessandro Armando, Luca Compagna, Silvio Ranise	System Description: RDL : Rewrite and Decision Procedure Laboratory.	IJCAR	2001	DBLP DOI BibTeX RDF
14	Panagiotis Manolios	Correctness of Pipelined Machines.	FMCAD	2000	DBLP DOI BibTeX RDF
14	Panagiotis Manolios, Kedar S. Namjoshi, Robert Summers	Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation.	CAV	1999	DBLP DOI BibTeX RDF
14	J Strother Moore	Proving Theorems About Java-Like Byte Code.	Correct System Design	1999	DBLP DOI BibTeX RDF
14	Stuart F. Oberman	Floating Point Division and Square Root Algorithms and Implementation in the AMD-K7 Microprocessor.	IEEE Symposium on Computer Arithmetic	1999	DBLP DOI BibTeX RDF
14	Jun Sawada, Warren A. Hunt Jr.	Processor Verification with Precise Exeptions and Speculative Execution.	CAV	1998	DBLP DOI BibTeX RDF
14	Jun Sawada, Warren A. Hunt Jr.	Trace Table Based Approach for Pipeline Microprocessor Verification.	CAV	1997	DBLP DOI BibTeX RDF