FAC: Vol 34, No 2

One of the major advantages of model checking over other formal methods is its ability to generate a counterexample when a model does not satisfy is its specification. A counterexample is an error trace that helps to locate the source of the error. ...

research-article

Open Access

Fast Automated Abstract Machine Repair Using Simultaneous Modifications and Refactoring

Article No.: 8, Pages 1–31https://doi.org/10.1145/3536430

Automated model repair techniques enable machines to synthesise patches that ensure models meet given requirements. B-repair, which is an existing model repair approach, assists users in repairing erroneous models in the B formal method, but repairing ...

research-article

Open Access

Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover

Article No.: 9, Pages 1–22https://doi.org/10.1145/3543670

We present a method for formal verification of transcendental hardware and software algorithms that scales to higher precision without suffering an exponential growth in runtimes. A class of implementations using piecewise polynomial approximation to ...

research-article

Open Access

Probabilistic Bigraphs

Article No.: 10, Pages 1–27https://doi.org/10.1145/3545180

Bigraphs are a universal computational modelling formalism for the spatial and temporal evolution of a system in which entities can be added and removed. We extend bigraphs to probabilistic bigraphs, and then again to action bigraphs, which include non-...