Shostak light

DOI10.1007/3-540-45620-1_28MaRDI QIDQ4809070zbMATH OpenFDO

Authors Harald Ganzinger

Publication date 12 August 2004

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2392/23920332.htm

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Recommendations

• On Shostak's decision procedure for combinations of theories
• Combining Shostak theories
• Combining non-stably infinite theories
• Functional Equations in Shostak Theories
• Model-theoretic methods in combined constraint satisfiability

Cited in

(8)

• Combination of convex theories: modularity, deduction completeness, and explanation
• Zero, successor and equality in BDDs
• Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
• Strategies for combining decision procedures
• Modular proof systems for partial functions with Evans equality
• Canonization for disjoint unions of theories
• Decision procedures for flat array properties
• On the verification of security-aware E-services

Describes a project that uses

Uses Software

• PVS

This page was built for publication: Shostak light

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