Die strategische Rolle der API: Umsetzung des Servicegedankens.

Autor: Dangl, Matthias matthias.dangl@ars.de

Publikováno v: IT Spektrum. 2024, Issue 4, p44-48. 5p.

Combining k-Induction with Continuously-Refined Invariants

Autor: Beyer, Dirk, Dangl, Matthias, Wendler, Philipp

Bounded model checking (BMC) is a well-known and successful technique for finding bugs in software. k-induction is an approach to extend BMC-based approaches from falsification to verification. Automatically generated auxiliary invariants can be used

Externí odkaz: http://arxiv.org/abs/1502.00096

Software Verification with PDR: An Implementation of the State of the Art

Autor: Beyer, Dirk, Dangl, Matthias

Publikováno v: Tools and Algorithms for the Construction and Analysis of Systems

Property-directed reachability (PDR) is a SAT/SMT-based reachability algorithm that incrementally constructs inductive invariants. After it was successfully applied to hardware model checking, several adaptations to software model checking have been

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=pmc_________::b6323a1b89fe805419eefef5386e1eb6
http://europepmc.org/articles/PMC7439737

Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.

Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses.

Autor: Beyer, Dirk, Dangl, Matthias

Publikováno v: Computer Aided Verification: 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II; 2016, p502-509, 8p