2 papers
cs.FL2025
Contract Based Program Models for Software Model Checking
Jesper Amilon, Dilian Gurov
Model checking temporal properties of software is algorithmically hard. To be practically feasible, it usually requires the creation of simpler, abstract models of the software, ov…
cs.LO2025
AutoDeduct: A Tool for Automated Deductive Verification of C Code
Jesper Amilon, Dilian Gurov, Christian Lidström +3
Deductive verification has become a mature paradigm for the verification of industrial software. Applying deductive verification, however, requires that every function in the code…