Seminar: Fortgeschrittene Techniken der Softwareverifikation (FTSV)
Dozentin: Prof. Dr. Marie-Christine Jakobs
Das Seminar wird nicht mehr länger angeboten. In diesem Seminar befassten wir uns mit Themen zu den aktuellen Forschungsinhalten der Arbeitsgruppe Semantik und Verifikation paralleler System. Es werden sowohl klassische als auch aktuelle Forschungsarbeiten im Bereich Softwareverifikation (d.h. Model Checking, Programmanalyse, Testen, etc.) behandelt.
Lerninhalte- und Ziele
Während des Seminars werden Sie unter Anleitung
- sich auf Basis von vorgegebener und selbst gefundener, wissenschaftlicher Literatur in Ihr Thema einarbeiten
- einen Vortrag über Ihr Thema vorbereiten und vor den anderen Teilnehmern halten, um mit ihnen anschließend über Ihr Thema zu diskutieren,
- eine wissenschaftliche Ausarbeitung verfassen, die einen zusammenfassenden Überblick über Ihr Thema gibt.
Nach erfolgreichem Abschluss des Seminars können sich die Studierenden anhand von Ausgangsliteratur eigenständig in ein wissenschaftliches Thema einarbeiten und dieses Thema einem heterogenen Fachpublikum sowohl mündlich als auch schriftlich präsentieren.
Im Detail können die Studierenden Methoden zur Literaturrecherche anwenden und die Relevanz von gefundener Literatur beurteilen. Sie können den wesentlichen Inhalt einer wissenschaftlichen Veröffentlichung ermitteln und diesen kritisch beurteilen. Außerdem sind sie in der Lage verschiedene wissenschaftliche Arbeiten miteinander zu vergleichen. In einem mündlichen Vortrag können die Studierenden ihr Thema und ihre Ergebnisse einem heterogenen Fachpublikum erklären und ihre Ergebnisse vor diesem Publikum verteidigen. Zusätzlich können die Studierenden in einer schriftlichen Ausarbeitung ihr Thema und ihre Ergebnisse beschreiben.
Vorkenntnisse
Empfohlen. Informatik- und Mathematikkenntnisse entsprechend den ersten 4 Semestern des Bachelorstudiengangs Informatik
Hilfreich. Besuch einer Veranstaltung des Fachgebietes Semantik und Verifikation paralleler Systeme
Seminarthemen vergangener Semester
In diesem Seminar beschäftigen wir uns mit Spezifikationssprachen und Zwischensprachen für die Verifikation. Spezifikationssprachen erlauben es Anforderungen, Annahmen und Garantien bezüglich funktionalen Verhaltens, etc. zu spezifizieren und mittels Verifikation zu prüfen. Zwischensprachen erlauben es einem Programme in verschiedenen Programmiersprachen mit dem gleichen Verifizierer zu analysieren. Gleichzeitig sind Zwischensprachen häufig darauf ausgelegt, die Verifikation zu vereinfachen, z.B. implizites Verhalten explizit zu machen, möglichst wenig Konstrukte zu verwenden ohne die Ausdrucksstärke zu verlieren, usw.
Zwischensprachen
- CIL: C Intermediate Language
George C. Necula, Scott McPeak, Shree Prakash Rahul, Westley Weimer: CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs. CC, LNCS 2304, pp. 213-228, Springer, 2002. - CIVL-C: Concurrency Intermediate Verification Language
Stephen F. Siegel, Manchun Zheng, Ziqing Luo, Timothy K. Zirkel, Andre V. Marianiello, John G. Edenhofner, Matthew B. Dwyer, Michael S. Rogers: CIVL: The Concurrency Intermediate Verification Language. SC, pp. 61:1-61:12, ACM, 2015. - LLVM IR: Low Level Virtual Machine Intermediate Representation
Chris Lattner, Vikram S. Adve: LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. CGO, pp. 75-88, IEEE, 2004.
Spezifikationssprachen
- FQL: FShell Query Language
Andreas Holzer, Michael Tautschnig, Christian Schallhart, Helmut Veith: An Introduction to Test Specification in FQL. HVC, LNCS 6504, pp. 9-22, Springer, 2010. - GOSPEL: Generic Ocaml SPEcification Language
Arthur Charguéraud, Jean-Christophe Filliâtre, Cláudio Lourenço, Mário Pereira: GOSPEL – Providing Caml with a Formal Specification Language. FM, LNCS 11800, pp. 484-501, Springer, 2019. - HILARE: High-Level ACSL Requirements with MetACSL
Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall: Tame Your Annotations with MetAcsl: Specifying, Testing and Proving High-Level Properties. TAP, LNCS , pp. 67-185, Springer, 2019. - JML: Java Modeling Language
Patrice Chalin, Joseph R. Kiniry, Gary T. Leavens, Erik Poll: Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2. FMCO, LNCS 4111, pp. 342-363, Springer, 2005. - Spec# Language
Mike Barnett, K. Rustan M. Leino, Wolfram Schulte: The Spec# Programming System: An Overview. CASSIS, LNCS 3362, pp. 49-69, Springer, 2004.
K. Rustan M. Leino, Peter Müller: Using the Spec# Language, Methodology, and Tools to Write Bug-Free Programs. LASER Summer School, LNCS 6029, pp. 91-139, Springer, 2008. - Specifications in the Eiffel Language
Bertrand Meyer: Applying „Design by Contract“. Computer 25(10): 40-51, 1992.
Zwischensprachen mit Spezifikationsanteil
- BoogiePL
Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, K. Rustan M. Leino: Boogie: A Modular Reusable Verifier for Object-Oriented Programs. FMCO, LNCS 4111, pp. 364-387, Springer, 2005. - Silver: Viper’s Intermediate Language
Peter Müller, Malte Schwerhoff, Alexander J. Summers: Viper: A Verification Infrastructure for Permission-Based Reasoning. VMCAI, LNCS 9583, pp. 41-62, 2016. - WhyML
Jean-Christophe Filliâtre, Andrei Paskevich: Why3 – Where Programs Meet Provers. ESOP, NCS 7792, pp. 125-128, Springer, 2013.
In diesem Seminar werden wir uns Werkzeuge zur Analyse und Verifikation von Softwareprogrammen widmen. Die Werkzeuge, die wir uns anschauen werden, unterscheiden sich in den Techniken und unterstützten Programmiersprachen. Im Detail werden wir uns die folgenden Werkzeugen anschauen.
Frameworks für Java Analyse
- Java PathFinder
Willem Visser, Klaus Havelund, Guillaume P. Brat, Seungjoon Park, Flavio Lerda: Model Checking Programs. Automated Software Engineering 10(2), pp. 203-232, 2003. - OPAL
Michael Eichberg, Ben Hermann: A Software Product Line for Static Analyses: The OPAL Framework. SOAP@PLDI, pp. 2:1-2:6, ACM, 2014.
Dominik Helm, Florian Kübler, Michael Reif, Michael Eichberg, Mira Mezini: Modular Collaborative Program Analysis in OPAL. FSE, pp. 184-196, ACM, 2020. - Soot
Patrick Lam, Eric Bodden, Ondřej Lhotá, and Laurie Hendren: The Soot Framework for Java Program Analysis: A Retrospective (wird in neuem Tab geöffnet). Cetus Users and Compiler Infastructure Workshop, 2011.
Frameworks für C Analyse
- Astrée
Patrick Cousot, Radhia Cousot, Jérôm Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, Xavier Rival: The ASTREÉ Analyzer. ESOP, LNCS 3444, pp. 21-30, Springer, 2005.
Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, avid Monniaux, Xavier Rival: A Static Analyzer for Large Safety-Critical Software. PLDI, pp. 196-207, ACM, 2003. - CPAchecker
Dirk Beyer, M. Erkan Keremoglu: CPAchecker: A Tool for Configurable Software Verification. CAV, LNCS 6806, pp. 184-190, Springer, 2011.
Dirk Beyer, Thomas A. Henzinger, Grégory Théoduloz: Program Analysis with Dynamic Precision Adjustment. ASE, pp. 29-38, IEEE, 2008. - Frama-C
Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, Boris Yakobowski: Frama-C – A Software Analysis Perspective. SEFM, LNCS 7504, pp. 233-247, Springer, 2012.
Patrick Baudin, François Bobot, David Bühler, Loïc Correnson, Florent Kirchner, Nikolai Kosmatov, André Maroneze, Valentin Perrelle, Virgile Prevosto, Julien Signoles, Nicky Williams: The Dogged Pursuit of Bug-Free C Programs: The Frama-C Software Analysis Platform. Commun.\ ACM 64(8), pp.\ 56-68, 2021.
Verifizierer für C Programme
- CBMC
Edmund M. Clarke, Daniel Kroening, Flavio Lerda: A Tool for Checking ANSI-C Programs. TACAS, LNCS 2988, pp. 168-176, Springer, 2004.
Edmund M. Clarke, Daniel Kroening, Karen Yorav: Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking. DAC, pp. 368-371, ACM, 2003. - ESBMC
Lucas C. Cordeiro, Bernd Fischer, João Marques-Silva: SMT-Based Bounded Model Checking for Embedded ANSI-C Software. IEEE TSE, 38(4), pp. 957-974, 2012. Mikhail Y. R. Gadelha, Felipe R. Monteiro, Jeremy Morse, Lucas C. Cordeiro, Bernd Fischer, Denis A. Nicole: ESBMC 5.0: An Industrial-Strength C Model CheckerESBMC 5.0: An Industrial-Strength C Model Checker. ASE, pp. 888-891, ACM, 2018 - Symbiotic
Jiri Slaby, Jan Strejcek, Marek Trtík: Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution. FMICS, LNCS 7437, pp. 207-221, Springer, 2012.
Marek Chalupa, Jan Strejcek, Martina Vitovská: Joint Forces for Memory Safety Checking. SPIN, LNCS 10869, pp. 115-132, Springer, 2018.
Marek Chalupa, Tomás Jasek, Jakub Novák, Anna Rechtácková, Veronika Soková, Jan Strejcek: Symbiotic 8: Beyond Symbolic Execution – (Competition Contribution). TACAS, LNCS 12652, pp. 453-457, Springer, 2021. - Ultimate Automizer
Matthias Heizmann, Jürgen Christ, Daniel Dietsch, Evren Ermis, Jochen Hoenicke, Markus Lindenmann, Alexander Nutz, Christian Schilling, Andreas Podelski: Ultimate Automizer with SMTInterpol – (Competition Contribution). TACAS, LNCS 7795, pp. 641-643, Springer, 2013.
Matthias Heizmann, Jochen Hoenicke, Andreas Podelski: Refinement of Trace Abstraction. SAS, LNCS 5673, pp. 69-85, Springer, 2009.
Matthias Heizmann, Jochen Hoenicke, Andreas Podelski: Nested Interpolants. POPL, pp. 471-482, ACM, 2010.
Verifizierer für Boogie Programme
- Boogie Verifizierer
Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, K. Rustan M. Leino: Boogie: A Modular Reusable Verifier for Object-Oriented Programs. FMCO, LNCS 4111, pp. 364-387, Springer, 2005. - Corral
Akash Lal, Shaz Qadeer, Shuvendu K. Lahiri: A Solver for Reachability Modulo Theories. CAV, LNCS 7358, pp. 427-443, Springer, 2012.
Akash Lal, Shaz Qadeer: Powering the Static Driver Verifier Using Corral. FSE, pp. 202-212, ACM, 2014.
Akash Lal, Shaz Qadeer: DAG Inlining: A Decision Procedure for Reachability-Modulo-Theories in Hierarchical Programs. PLDI, pp. 280-290, ACM, 2015.
Diese Seminar behandelt Themen aus dem Bereich automatischer Testfallgenerierung. Das Ziel der Testfallgenerierung ist es Testeingaben zu erzeugen, die Fehler in Programmen entdecken, oder eine Menge von Testeingaben zu erzeugen, die zusammen ein gewisses Überdeckungskriterium erreichen. Konkrekt beschäftigen wir uns in diesem Seminar mit Werkzeugen zur automatischen Testgenerierung, die ihre Testeingaben (1) zufallsbasiert, (2) mit such-basierten Ansätzen, (3) mit Hilfe von symbolischer Ausführung oder (4) mit Hilfe von Erreichbarkeitsanalysen generieren.
Random Test Generation
- QuickCheck
Koen Claessen, John Hughes: QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs. ICFP, pp. 268-279, ACM, 2000. - Randoop
Carlos Pacheco, Shuvendu K. Lahiri, Michael D. Ernst, Thomas Ball: Feedback-Directed Random Test Generation. ICSE, pp. 75-84, IEEE 2007.
Search-based Test Generation
- Korat
Chandrasekhar Boyapati, Sarfraz Khurshid, Darko Marinov: Korat: Automated Testing Based on Java Predicates. ISSTA, pp. 123-133, ACM, 2002. - EvoSuite
Gordon Fraser, Andrea Arcuri: Evolutionary Generation of Whole Test Suites. QSIC, pp. 31-40, IEEE, 2011.
Test Generation with Symbolic Execution
- KLEE
Cristian Cadar, Daniel Dunbar, Dawson R. Engler: KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs (wird in neuem Tab geöffnet). OSDI, pp. 209-224, USENIX, 2008. - PathCrawler
Nicky Williams, Bruno Marre, Patricia Mouy, Muriel Roger: PathCrawler: Automatic Generation of Path Tests by Combining Static and Dynamic Analysis. EDCC, pp. 281-292, Springer, 2005. - Pex
Nikolai Tillmann, Jonathan de Halleux: Pex-White Box Test Generation for .NET. TAP, pp. 134-153, Springer, 2008. - CUTE
Koushik Sen, Darko Marinov, Gul Agha: CUTE: A Concolic Unit Testing Engine for C. FSE, pp. 263-272, ACM, 2005. - SAGE
Patrice Godefroid, Michael Y. Levin, David A. Molnar: Automated Whitebox Fuzz Testing. NDSS 2008
Test Generation with Reachability Analyses
- Blast
Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar: Generating Tests from Counterexamples. ICSE, pp. 326-335, IEEE, 2004. - FShell
Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith: FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement. CAV, pp. 209-213, Springer, 2008.
Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith: Query-Driven Program Testing. VMCAI, pp. 151-166, Springer, 2009. - CoVeriTest
Dirk Beyer, Marie-Christine Jakobs: CoVeriTest: Cooperative Verifier-Based Testing. FASE, pp. 389-408, Springer, 2019.
Diese Seminar behandelt Themen unseres Forschungsbereichs Überprüfung von Verifikationsergebnissen. Das Ziel der Prüfung ist es, das Vertrauen in das Verifikationsergebnis zu stärken. So kann man z.B. prüfen, ob die Verifikation tatsächlich durchgeführt wurde und ob das Verifikationswerkzeug fehlerfrei gearbeitet hat. In diesem Seminar beschäftigen wir uns mit (1) verschiedenen Protokollen der Prüfung, mit (2) Prüftechniken für Datenflussanalysen, abstrakter Interpretation, oder Model Checking.
Prüfprotokolle
- Proof-Carrying Code
George C. Necula: Enforcing Security and Safety with Proof-Carrying Code, MFPS 1999.
George C. Necula, Peter Lee: Safe, Untrusted Agents Using Proof-Carrying Code, Mobile Agents and Security 1998. - Programs from Proofs
Daniel Wonisch, Alexander Schremmer, Heike Wehrheim: Programs from Proofs – A PCC Alternative, CAV 2013. - Certifying Algorithms
Ross M. McConnell, Kurt Mehlhorn, Stefan Näher, Pascal Schweitzer: Certifying algorithms, Comput. Sci. Rev. 5(2), 2011. - Amanat Protocol
Sagar Chaki, Christian Schallhart, Helmut Veith: Verification Across Intellectual Property Boundaries, CAV 2007. - Violation and Correctness Witnesses
Dirk Beyer, Matthias Dangl, Daniel Dietsch, Matthias Heizmann, Andreas Stahlbauer: Witness validation and stepwise testification across software verifiers, FSE 2015.
Dirk Beyer, Matthias Dangl, Daniel Dietsch, Matthias Heizmann: Correctness witnesses: exchanging verification results between verifiers, FSE 2016.
Prüftechniken für Model Checking
- Temporal Safety Proofs
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, George C. Necula, Grégoire Sutre, Westley Weimer: Temporal-Safety Proofs for Systems Code, CAV 2002. - Extreme Model Checking
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Marco A. A. Sanvido: Extreme Model Checking, Verification: Theory and Practice 2003.
Prüftechniken für Datenflussanalysen und abstrakte Interpretation
- Lightweight Bytecode Verification
Eva Rose: Lightweight Bytecode Verification, J. Autom. Reason. 31(3-4), 2003. - Validating Dataflow Annotations
Wolfram Amme, Marc-André Möller, Philipp Adler: Data Flow Analysis as a General Concept for the Transport of Verifiable Program Annotations, Electron. Notes Theor. Comput. Sci. 176(3), 2007. - Hoare Proofs from Abstract Interpretation
Sunae Seo, Hongseok Yang, Kwangkeun Yi: Automatic Construction of Hoare Proofs from Abstract Interpretation Results, APLAS 2003. - Abstraction-Carrying Code
Elvira Albert, Germán Puebla, Manuel V. Hermenegildo: Abstraction-Carrying Code, LPAR 2004. - Configurable Program Certification
Marie-Christine Jakobs, Heike Wehrheim: Certification for configurable program analysis, SPIN 2014.
Marie-Christine Jakobs: Speed Up Configurable Certificate Validation by Certificate Reduction and Partitioning, SEFM 2015.
Diese Seminar behandelt Themen unseres Forschungsbereichs Kombination von Verifikationsverfahren. Insbesondere beschäftigen wir uns mit kooperativen Verifikationsverfahren. Das Ziel kooperativer Verifikationsverfahren ist die verschiedenen Stärken und Schwächen der Verifikationsverfahren zu nutzen und mächtigere Verfahren mittels Kooperation zu erreichen. In diesem Seminar beschäftigen wir uns mit drei Arten von Kooperationen (1) Bestätigung von Alarmen, (2) Aufteilung des Verifikationsaufwands und (3) algorithmische Integration von verschiedenen Verifikationsansätzen.
Ziel der Bestätigung von Alarmen ist die Anzahl der falschen Alarme zu reduzieren und den Entwicklern nur Alarme zu zeigen, die tatsächlich mit einen Testfall bestätigt und nachvollzogen werden können.
Bei der Aufteilung des Verifikationsaufwands werden verschiedene Teilaspekte oder verschiedene Teile des Programms von unterschiedlichen Verfahren geprüft. Häufig werden sequentielle Kombinationen genutzt, in denen das zweite Verifikationswerkzeug lediglich die übrig gebliebenen Beweisverpflichtungen prüfen muss.
In der algorithmische Integration von verschiedenen Verifikationsansätzen werden neue Verifikationsalgorithmen entwickelt die existierende Ansätze als Teilkomponenten nutzen.
Bestätigung von Alarmen
- Check’n’Crash
Christoph Csallner, Yannis Smaragdakis: Check 'n' crash: combining static checking and testing. ICSE 2005. - DSD-Crasher
Christoph Csallner, Yannis Smaragdakis: DSD-Crasher: a hybrid analysis tool for bug finding. ISSTA 2006. - SANTE: Static Analysis and Testing
Omar Chebaro, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand: Program slicing enhances a verification technique combining static and dynamic analysis. SAC 2012. - Tests from Witnesses
Dirk Beyer, Matthias Dangl, Thomas Lemberger, Michael Tautschnig: Tests from Witnesses – Execution-Based Validation of Verification Results. TAP 2018.
Aufteilung des Verifikationsaufwands
- Failure-Directed Program Trimming
Kostas Ferles, Valentin Wüstholz, Maria Christakis, Isil Dillig: Failure-directed program trimming. ESEC/SIGSOFT FSE 2017 - Collaboration via Verification Annotations
Maria Christakis, Peter Müller, Valentin Wüstholz: Guiding dynamic symbolic execution toward unverified program executions. ICSE 2016. - CoDiDroid: Cooperative Android Analysis
Felix Pauck, Heike Wehrheim: Together strong: cooperative Android app analysis. ESEC/SIGSOFT FSE 2019.
Algorithmische Integration von verschiedenen Verifikationsansätzen
- Combining k-Induction with Invariant Generation
Dirk Beyer, Matthias Dangl, Philipp Wendler: Boosting k-Induction with Continuously-Refined Invariants. CAV 2015. - Synergy: Using Test Generation for Counterexample Check and Identification of Refinement State
Bhargav S. Gulavani, Thomas A. Henzinger, Yamini Kannan, Aditya V. Nori, Sriram K. Rajamani: SYNERGY: a new algorithm for property checking. FSE 2006. - Dash: Using Test Generation for Counterexample Check and Refinement
Ashutosh Gupta, Rupak Majumdar, Andrey Rybalchenko: From Tests to Proofs. TACAS 2009. - Ufo: Integrating Under-Approximations and Over-Approximations
Aws Albarghouthi, Arie Gurfinkel, Marsha Chechik: From Under-Approximations to Over-Approximations and Back. TACAS 2012. - kIkI: Combining k-Invariants with k-Induction
Martin Brain, Saurabh Joshi, Daniel Kroening, Peter Schrammel: Safety Verification and Refutation by k-Invariants and k-Induction. SAS 2015.
Das Seminar ist aufgrund fehlender Teilnehmer ausgefallen und wird daher im folgenden Semester mit den gleichen Themen wieder angeboten.
Diese Seminar behandelt Themen unseres Forschungsbereichs inkrementelle Verifikation. Techniken der inkrementellen Verifikation sind eine Schlüsseltechnologie, um formale Verifikation in agilen Softwareprojekten einzusetzen. Um mit den vielen, schnellen Änderungen mithalten zu können. Umfasst inkrementelle Verifikation Techniken, die eine erneute Verifikation nach einer Programmänderung effizienter machen. Dafür nutzt inkrementelle Verifikation Informationen aus einer vorherigen Verifikation. Die Art der Information und ihrer Nutzung unterscheidet sich. Im Seminar betrachten wir vier Klassen von inkrementeller Verifikation: funktionale Äquivalenzprüfung, Nutzung von Zwischenergebnissen, Beweisadaption, und Beschränkung der Verifikation auf modifizierte Ausführungspfade.
Verfahren zu funktionalen Äquivalenzprüfung prüfen, ob modifizierte Programmteile (typischerweise Funktionen) das gleiche Ein- und Ausgabeverhalten zeigen wie der entsprechende Programmteil nach der Verifikation.
Verfahren, die Zwischenergebnisse wiederverwenden, vermeiden das Wiederentdecken von bereits bekannten Informationen, z.B. Invarianten, Antworten auf Erfüllbarkeitsanfragen, und Abstraktionsgrad. Ihre Annahme ist das viele dieser Informationen weiterhin gültig und benötigt werden.
In der Beweisadaption wird geprüft, welche Teile des Beweises weiterhin gültig sind. Gültige Beweisteile werden übernommen. Ungültige Beweisteile werden gelöscht und nur der die fehlenden Beweisteile wird durch erneute Verifikation wiederhergestellt.
Die letzte Klasse ist verwandt mit Beweisadaptionen. Verfahren, die sich auf modifizierte Pfade beschränken, stoppen die Verifikation von Pfaden sobald keine Veränderung mehr erreicht werden kann oder führen leichtgewichtige Verifikationsschritte aus solange noch keine Veränderung gesehen wurde.
Funktionale Äquivalenzprüfung
- Regression Verification
Benny Godlin, Ofer Strichman: Regression verification. DAC 2009 - Relation Regression Verification
Dennis Felsing, Sarah Grebing, Vladimir Klebanov, Philipp Rümmer, Mattias Ulbrich: Automating regression verification. ASE 2014 - UCKlee
David A. Ramos, Dawson R. Engler: Practical, Low-Effort Equivalence Verification of Real Code. CAV 2011
Wiederverwendung von Zwischenergebnissen
- Constraints Reuse
Willem Visser, Jaco Geldenhuys, Matthew B. Dwyer: Green: reducing, reusing and recycling constraints in program analysis. FSE 2012 - Precision Reuse
Dirk Beyer, Stefan Löwe, Evgeny Novikov, Andreas Stahlbauer, Philipp Wendler: Precision reuse for efficient regression verification. ESEC/SIGSOFT FSE 2013 - Reusing Trace Abstractions
Bat-Chen Rothenberg, Daniel Dietsch, Matthias Heizmann: Incremental Verification Using Trace Abstraction. SAS 2018
Beweisadaption
- Incremental Upgrade Checking
Ondrej Sery, Grigory Fedyukovich, Natasha Sharygina: Incremental upgrade checking by means of interpolation-based function summaries. FMCAD 2012 - Extreme Model Checking
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Marco A. A. Sanvido: Extreme Model Checking. Verification: Theory and Practice 2003
Überspringen von Verifikationsschritten
- Directed Incremental Verification
Suzette Person, Guowei Yang, Neha Rungta, Sarfraz Khurshid: Directed incremental symbolic execution. PLDI 2011 - Memoized Symbolic Execution
Guowei Yang, Corina S. Pasareanu, Sarfraz Khurshid: Memoized symbolic execution. ISSTA 2012 - Regression Model Checking
Guowei Yang, Matthew B. Dwyer, Gregg Rothermel: Regression model checking. ICSM 2009 - iCoq
Ahmet Çelik, Karl Palmskog, Milos Gligoric: iCoq: regression proof selection for large-scale verification projects. ASE 2017 - iAlloy
Wenxi Wang, Kaiyuan Wang, Milos Gligoric, Sarfraz Khurshid: Incremental Analysis of Evolving Alloy Models. TACAS 2019