Automated reasoning techniques based on computer algebra have seen renewed interest in recent years and are for example heavily used in formal verification of arithmetic circuits. However, the verification process might contain errors. Generating …
verfasst von:
Daniela Kaufmann, Mathias Fleury, Armin Biere, Manuel Kauers
Program verification is a resource-hungry task. This paper looks at the problem of parallelizing SMT-based automated program verification, specifically bounded model-checking, so that it can be distributed and executed on a cluster of machines. We …
Reactive synthesis is a key technique for the design of correct-by-construction systems, which has been thoroughly investigated in the last decades. It consists of the synthesis of a controller that reacts to environment’s inputs satisfying a …