DKAL and Z3: A Logic Embedding Experiment

DOI10.1007/978-3-642-15025-8_25zbMath1287.68153OpenAlexW1579159551MaRDI QIDQ3586018

Sergio Mera, Nikolaj Bjørner

Publication date: 3 September 2010

Published in: Fields of Logic and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-15025-8_25

zbMATH Keywords

embeddingmodel extractionDKALZ3

Mathematics Subject Classification ID

Uses Software

• SLAM
• Spec#
• z3
• DKAL
• BoogiePL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Decidability and complexity of simultaneous rigid E-unification with one variable and related results
• Back to the future
• Efficient E-Matching for SMT Solvers
• Linear Functional Fixed-points

This page was built for publication: DKAL and Z3: A Logic Embedding Experiment