Ausgabe 1-4/2018
Special Issue: Milestones in Interactive Theorem Proving
Inhalt (14 Artikel)
Introduction to Milestones in Interactive Theorem Proving
Jeremy Avigad, Jasmin Christian Blanchette, Gerwin Klein, Lawrence Paulson, Andrei Popescu, Gregor Snelting
Open Access
The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar
Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk
Distant Decimals of : Formal Proofs of Some Algorithms Computing Them and Guarantees of Exact Computation
Yves Bertot, Laurence Rideau, Laurent Théry
CoSMed: A Confidentiality-Verified Social Media Platform
Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi
Toward Compositional Verification of Interruptible OS Kernels and Device Drivers
Hao Chen, Xiongnan Wu, Zhong Shao, Joshua Lockerman, Ronghui Gu
Open Access
Verified iptables Firewall Analysis and Verification
Cornelius Diekmann, Lars Hupel, Julius Michaelis, Maximilian Haslbeck, Georg Carle
Open Access
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich, Christoph Weidenbach
VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs
Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds, Andrew W. Appel
Formally Verified Algorithms for Upper-Bounding State Space Diameters
Mohammad Abdulaziz, Michael Norrish, Charles Gretton
Regular Language Representations in the Constructive Type Theory of Coq
Christian Doczkal, Gert Smolka