In: International journal on software tools for technology transfer, 2021, p. 15
The use of propositional logic and systems of linear inequalities over reals is a common means to model software for formal verification. Craig interpolants constitute a central building block in this setting for over-approximating reachable states, e.g. as candidates for inductive loop invariants. Interpolants for a linear system can be efficiently computed from a Simplex refutation by ...
|
In: Formal Methods in System Design, 2014, vol. 45, no. 1, p. 63-109
|
Thèse de doctorat : Università della Svizzera italiana, 2016 ; 2016INFO009.
Model checking is a well established technique to verify systems, exhaustively and automatically. The state space explosion, known as the main difficulty in model checking scalability, has been successfully approached by symbolic model checking which represents programs using logic, usually at the propositional or first order theories level. Craig interpolation is one of the most successful...
|
Thèse de doctorat : Università della Svizzera italiana, 2015 ; 2015INFO013.
Software continuously evolves to meet rapidly changing human needs. Each evolved transformation of a program is expected to preserve important correctness and security properties. Aiming to assure program correctness after a change, formal verification techniques, such as Software Model Checking, have recently benefited from fully automated solutions based on symbolic reasoning and...
|
Thèse de doctorat : Università della Svizzera italiana, 2013 ; 2013INFO006.
Model checking is one of the most appreciated methods for automated formal verification of software and hardware systems. The main challenge in model checking, i.e. scalability to complex systems of extremely large size, has been successfully addressed by means of symbolic techniques, which rely on an efficient representation and manipulation of the systems based on first order logic....
|
