概述

1. ATVA

   Verified Textbook Algorithms. A Biased Survey Nipkow, Tobias, Eberl, Manuel, and Haslbeck, Maximilian P. L. In ATVA 2020, Automated Technology for Verification and Analysis 2020

验证框架

1. ICFP

   Program Verification through Characteristic Formulae Charguéraud, Arthur In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming 2010 [Abs]

   This paper describes CFML, the first program verification tool based on characteristic formulae. Given the source code of a pure Caml program, this tool generates a logical formula that implies any valid post-condition for that program. One can then prove that the program satisfies a given specification by reasoning interactively about the characteristic formula using a proof assistant such as Coq. Our characteristic formulae improve over Honda et al’s total characteristic assertion pairs in that they are expressible in standard higher-order logic, allowing to exploit them in practice to verify programs using existing proof assistants. Our technique has been applied to formally verify more than half of the content of Okasaki’s Purely Functional Data Structures reference book

2. ICFP

   Characteristic Formulae for the Verification of Imperative Programs Charguéraud, Arthur In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming 2011 [Abs]

   In previous work, we introduced an approach to program verification based on characteristic formulae. The approach consists of generating a higher-order logic formula from the source code of a program. This characteristic formula is constructed in such a way that it gives a sound and complete description of the semantics of that program. The formula can thus be exploited in an interactive proof assistant to formally verify that the program satisfies a particular specification.This previous work was, however, only concerned with purely-functional programs. In the present paper, we describe the generalization of characteristic formulae to an imperative programming language. In this setting, characteristic formulae involve specifications expressed in the style of Separation Logic. They also integrate the frame rule, which enables local reasoning. We have implemented a tool based on characteristic formulae. This tool, called CFML, supports the verification of imperative Caml programs using the Coq proof assistant. Using CFML, we have formally verified nontrivial imperative algorithms, as well as CPS functions, higher-order iterators, and programs involving higher-order stores.

3. ITP

   Automatic Data Refinement Lammich, Peter In Interactive Theorem Proving 2013 [Abs]

   We present the Autoref tool for Isabelle/HOL, which automatically refines algorithms specified over abstract concepts like maps and sets to algorithms over concrete implementations like red-black-trees, and produces a refinement theorem. It is based on ideas borrowed from relational parametricity due to Reynolds and Wadler.

4. ITP

   Refinement to Imperative HOL Lammich, Peter J. Autom. Reason. 2019 [Abs]

   Many algorithms can be implemented most efficiently with imperative data structures. This paper presents Sepref, a stepwise refinement based tool chain for the verification of imperative algorithms in Isabelle/HOL. As a back end we use imperative HOL, which allows to generate verified imperative code. On top of imperative HOL, we develop a separation logic framework with powerful proof tactics. We use this framework to verify basic imperative data structures and to define a refinement calculus between imperative and functional programs. We provide a tool to automatically synthesize a concrete imperative program and a refinement proof from an abstract functional program, selecting implementations of abstract data types according to a user-provided configuration. As a front end to describe the abstract programs, we use the Isabelle Refinement Framework, for which many algorithms have already been formalized. Our tool chain is complemented by a large selection of verified imperative data structures. We have used Sepref for several verification projects, resulting in efficient verified implementations that are competitive with unverified ones in Java or C$++$++.

5. JAR

   Automatic Refinement to Efficient Data Structures: A Comparison of Two Approaches Lammich, Peter, and Lochbihler, Andreas J. Autom. Reason. 2019
6. CPP

   Higher-Order Representation Predicates in Separation Logic Charguéraud, Arthur In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs 2016 [Abs]

   In Separation Logic, representation predicates are used to describe mutable data structures, by establishing a relationship between the entry point of the structure, the piece of heap over which this structure spans, and the logical model associated with the structure. When a data structure is polymorphic, such as in the case of a container, its representation predicate needs to be parameterized not just by the type of the items stored in the structure, but also by the representation predicates associated with these items. Such higher-order representation predicates can be used in particular to control whether containers should own their items. In this paper, we present, through a collection of practical examples, solutions to the challenges associated with reasoning about accesses into data structures that own their elements.

7. JFP

   Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code Breitner, Joachim, Spector-Zabusky, Antal, Li, Yao, Rizkallah, Christine, Wiegley, John, Cohen, Joshua, and Weirich, Stephanie J. Funct. Program. 2021
8. TACAS

   Efficient Verification of Imperative Programs Using Auto2 Zhan, Bohua In Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part I 2018

搜索和排序

1. IJCAR

   Efficient Verified Implementation of Introsort and Pdqsort Lammich, Peter In Automated Reasoning 2020 [Abs]

   Sorting algorithms are an important part of most standard libraries, and both, their correctness and efficiency is crucial for many applications.

数据结构

1. ITP

   Automatic Functional Correctness Proofs for Functional Search Trees Nipkow, Tobias In Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings 2016
2. APLAS

   Verified Root-Balanced Trees Nipkow, Tobias In Programming Languages and Systems - 15th Asian Symposium, APLAS 2017, Suzhou, China, November 27-29, 2017, Proceedings 2017
3. ITP

   Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra Lammich, Peter, and Nipkow, Tobias In 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA 2019
4. CPP

   Proof pearl: Braun trees Nipkow, Tobias, and Sewell, Thomas In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020 2020

图论算法

1. ITP

   Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm Lammich, Peter In Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings 2014
2. CPP

   A Framework for Verifying Depth-First Search Algorithms Lammich, Peter, and Neumann, René In Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015 2015
3. MFCS

   Trustworthy Graph Algorithms (Invited Talk) Abdulaziz, Mohammad, Mehlhorn, Kurt, and Nipkow, Tobias In 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019, August 26-30, 2019, Aachen, Germany 2019
4. ITP

   Formal Proof and Analysis of an Incremental Cycle Detection Algorithm Guéneau, Armaël, Jourdan, Jacques-Henri, Charguéraud, Arthur, and Pottier, François In 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA 2019
5. JAR

   Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL Lammich, Peter, and Sefidgar, S. Reza J. Autom. Reason. 2019
6. ITP

   Formal Proofs of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq and Isabelle Chen, Ran, Cohen, Cyril, Lévy, Jean-Jacques, Merz, Stephan, and Théry, Laurent In 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA 2019
7. OOPSLA

   Certifying graph-manipulating C programs via localizations within data structures Wang, Shengyi, Cao, Qinxiang, Mohan, Anshuman, and Hobor, Aquinas Proc. ACM Program. Lang. 2019

其它算法

1. JAR

   Proof Pearl: Mechanizing the Textbook Proof of Huffman’s Algorithm Blanchette, Jasmin Christian J. Autom. Reason. 2009
2. ITP

   Verified Memoization and Dynamic Programming Wimmer, Simon, Hu, Shuwei, and Nipkow, Tobias In Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings 2018
3. IJCAR

   Verification of Closest Pair of Points Algorithms Rau, Martin, and Nipkow, Tobias In Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II 2020

时间复杂度的验证

1. ESOP

   Amortised Resource Analysis with Separation Logic Atkey, Robert In Programming Languages and Systems, 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings 2010
2. JAR

   Proving Divide and Conquer Complexities in Isabelle/HOL Eberl, Manuel J. Autom. Reason. 2017
3. ESOP

   A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification Guéneau, Armaël, Charguéraud, Arthur, and Pottier, François In Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings 2018
4. IJCAR

   Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle Zhan, Bohua, and Haslbeck, Maximilian P. L. In Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings 2018
5. ITP

   Amortized Complexity Verified Nipkow, Tobias In Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings 2015
6. JAR

   Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits Charguéraud, Arthur, and Pottier, François J. Autom. Reason. 2019
7. ITP

   Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL Haslbeck, Maximilian P. L., and Lammich, Peter In 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA 2019

随机算法的验证

1. ESOP

   A Verified Compiler for Probability Density Functions Eberl, Manuel, Hölzl, Johannes, and Nipkow, Tobias In Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings 2015
2. ITP

   Verified Analysis of Random Binary Tree Structures Eberl, Manuel, Haslbeck, Max W., and Nipkow, Tobias In Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings 2018

模拟检验算法的验证

1. TACAS

   Verifying pCTL Model Checking Hölzl, Johannes, and Nipkow, Tobias In Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings 2012
2. CAV

   A Fully Verified Executable LTL Model Checker Esparza, Javier, Lammich, Peter, Neumann, René, Nipkow, Tobias, Schimpf, Alexander, and Smaus, Jan-Georg In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings 2013
3. NFM

   Formal Verification of an Executable LTL Model Checker with Partial Order Reduction Brunner, Julian, and Lammich, Peter In NASA Formal Methods - 8th International Symposium, NFM 2016, Minneapolis, MN, USA, June 7-9, 2016, Proceedings 2016
4. JAR

   Markov Chains and Markov Decision Processes in Isabelle/HOL Hölzl, Johannes J. Autom. Reason. 2017
5. TACAS

   Verified Model Checking of Timed Automata Wimmer, Simon, and Lammich, Peter In Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part I 2018

人工智能算法的验证

1. ICML

   Developing Bug-Free Machine Learning Systems With Formal Mathematics Selsam, Daniel, Liang, Percy, and Dill, David L. In Proceedings of the 34th International Conference on Machine Learning, ICML 2017, Sydney, NSW, Australia, 6-11 August 2017 2017
2. ICTAI

   A Formally Verified Validator for Classical Planning Problems and Solutions Abdulaziz, Mohammad, and Lammich, Peter In IEEE 30th International Conference on Tools with Artificial Intelligence, ICTAI 2018, 5-7 November 2018, Volos, Greece 2018
3. ITP

   A Formal Proof of the Expressiveness of Deep Learning Bentkamp, Alexander, Blanchette, Jasmin Christian, and Klakow, Dietrich In Interactive Theorem Proving - 8th International Conference, ITP 2017, Brası́lia, Brazil, September 26-29, 2017, Proceedings 2017