Distributing the workload in a lazy theorem-prover

DOI10.1016/J.ENTCS.2007.03.013MaRDI QIDQ2870323zbMATH OpenOpenAlexFDO

Authors David Déharbe, Silvio Ranise, J. Vidal

Publication date 17 January 2014

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2007.03.013

zbMATH Keywords

automated theorem provingdistributed computingSMT prover

Mathematics Subject Classification ID

Distributed systems (68M14) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Distributing equational theorem proving
• Theorem proving using lazy proof explication.
• scientific article; zbMATH DE number 1254024
• scientific article; zbMATH DE number 512823
• scientific article; zbMATH DE number 4164187

Cites work

• A machine program for theorem-proving
• Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
• Artificial Intelligence and Symbolic Computation
• Computer Aided Verification
• Computer Aided Verification
• Computer Aided Verification
• Counterexample-guided abstraction refinement for symbolic model checking
• Efficient distributed SAT and SAT-based distributed bounded model checking
• Graph-Based Algorithms for Boolean Function Manipulation
• GridSAT: Design and implementation of a computational grid application
• scientific article; zbMATH DE number 1809862 (Why is no real title available?)
• scientific article; zbMATH DE number 2080047 (Why is no real title available?)
• Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
• Simplification by Cooperating Decision Procedures
• The discrete time TOOLBUS. -- A software coordination architecture
• Theorem proving using lazy proof explication.
• Theoretical Aspects of Computing - ICTAC 2004

Cited in

(3)

• Lazy techniques for fully expansive theorem proving
• Distributing equational theorem proving
• Theorem proving using lazy proof explication.

Describes a project that uses

Uses Software

• Zapato
• ToolBus
• Chaff
• CVC Lite
• GridSAT
• E Theorem Prover

This page was built for publication: Distributing the workload in a lazy theorem-prover

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2870323)