Smtlink 2.0
Y Peng, MR Greenstreet - arXiv preprint arXiv:1810.04317, 2018 - arxiv.org
Smtlink is an extension of ACL2 with Satisfiability Modulo Theories (SMT) solvers. We
presented an earlier version at ACL2'2015. Smtlink 2.0 makes major improvements over the …
presented an earlier version at ACL2'2015. Smtlink 2.0 makes major improvements over the …
Extending ACL2 with SMT solvers
Y Peng, M Greenstreet - arXiv preprint arXiv:1509.06082, 2015 - arxiv.org
We present our extension of ACL2 with Satisfiability Modulo Theories (SMT) solvers using
ACL2's trusted clause processor mechanism. We are particularly interested in the …
ACL2's trusted clause processor mechanism. We are particularly interested in the …
Prototyping games using formal methods
Courses on formal methods are often based on examples and case studies, which are
supposed to show students how to apply formal methods in practice. However, examples …
supposed to show students how to apply formal methods in practice. However, examples …
Proof assisted symbolic model checking for B and Event-B
S Krings, M Leuschel - Abstract State Machines, Alloy, B, TLA, VDM, and Z …, 2016 - Springer
We have implemented various symbolic model checking algorithms, like BMC, k-Induction
and IC3 for B and Event-B. The high-level nature of B and Event-B accounts for complicated …
and IC3 for B and Event-B. The high-level nature of B and Event-B accounts for complicated …
Comparing EvenB, and Why3 Models of Sparse Sets
M Cristiá, C Dubois - arXiv preprint arXiv:2307.03974, 2023 - arxiv.org
Many representations for sets are available in programming languages libraries. The paper
focuses on sparse sets used, eg, in some constraint solvers for representing integer variable …
focuses on sparse sets used, eg, in some constraint solvers for representing integer variable …
Analysing ProB's Constraint Solving Backends: What Do They Know? Do They Know Things? Let's Find Out!
J Dunkelau, J Schmidt, M Leuschel - International Conference on Rigorous …, 2020 - Springer
We evaluate the strengths and weaknesses of different backends of the ProB constraint
solver. For this, we train a random forest over a database of constraints to classify whether a …
solver. For this, we train a random forest over a database of constraints to classify whether a …
SMT-based generation of symbolic automata
Open pNets are formal models that can express the behaviour of open systems, either
synchronous, asynchronous, or heterogeneous. They are endowed with a symbolic …
synchronous, asynchronous, or heterogeneous. They are endowed with a symbolic …
Integrating SMT with theorem proving for analog/mixed-signal circuit verification
Y Peng, M Greenstreet - NASA Formal Methods Symposium, 2015 - Springer
We present our integration of the Z3 SMT solver into the ACL2 theorem prover and its
application to formal verification of analog-mixed signal circuits by proving global …
application to formal verification of analog-mixed signal circuits by proving global …
[HTML][HTML] Validating and verifying the requirements and design of a haemodialysis machine using the Rodin toolset
We present a formal specification and analysis of a haemodialysis machine (HD machine) in
Event-B using the Rodin Toolset. The medical device domain is a particularly complex …
Event-B using the Rodin Toolset. The medical device domain is a particularly complex …
Using SMT engine to generate symbolic automata
X Qin, S Bliudze, E Madelaine… - … International Workshop on …, 2018 - inria.hal.science
Open pNets are used to model the behaviour of open systems, both synchronous or
asynchronous, expressed in various calculi or languages. They are endowed with a …
asynchronous, expressed in various calculi or languages. They are endowed with a …