The bedrock structured programming system by Chlipala, A

“…We report on the design and implementation of an extensible programming language and its intrinsic support for formal verification. Our language is targeted at low-level programming of infrastructure like operating systems and runtime systems. …”
Get full text

PROLEAD by Nicolai Müller, Amir Moradi

“…Moreover, abstract models like probing security allow formal verification tools to evaluate masked implementations. …”
Get full text

Towards Neural Routing with Verified Bounds on Performance by Igor Petrovich Buzhinsky, Anatoly Abramovich Shalyto

“…On the way to compensate for this drawback, formal verification techniques, which can provide reliable guarantees on program behavior, were developed for DNNs. …”
Get full text

VConMC: Enabling Consistency Verification for Distributed Systems Using Implementation-Level Model Checkers and Consistency Oracles by Beom-Heyn Kim

“…However, formal verification is not a panacea due to limitations such as the cost of verification, inability to verify existing implementations, and human errors involved. …”
Get full text

Verification of HotStuff BFT Consensus Protocol With TLA+/TLC in an Industrial Setting by Kukharenko Vladimir, Ziborov Kirill, Sadykov Rafael, Rezin Ruslan

“…The extent of formal verification methods applied in industrial projects has always been limited. …”
Get full text

How to Formalize Loop Iterations in Cryptographic Protocols Using ProVerif by Takehiko Mieno, Hiroyuki Okazaki, Kenichi Arai, Yuichi Futa

“…The formal verification of cryptographic protocols has been extensively studied in recent years. …”
Get full text

PROLEAD by Nicolai Müller, Amir Moradi

“…Moreover, abstract models like probing security allow formal verification tools to evaluate masked implementations. …”
Get full text

Methods for Domain Specification of Verification-Oriented Process Ontology by Natalia O. Garanina, Igor S. Anureev, Olesya I. Borovikova, Vladimir E. Zyubin

“…One of the advantages of such ontologies is their formal semantics which make possible formal verification of the described systems. Our method is based on the abstract verification-oriented process ontology. …”
Get full text

Certifying checksum-based logging in the RapidFSCQ crash-safe filesystem by Wang, Stephanie, M. Eng Massachusetts Institute of Technology

Get full text

The bedrock structured programming system by Chlipala, Adam

“…We report on the design and implementation of an extensible programming language and its intrinsic support for formal verification. Our language is targeted at low-level programming of infrastructure like operating systems and runtime systems. …”
Get full text

Verified Approximation Algorithms by Robin Eßmann, Tobias Nipkow, Simon Robillard, Ujkan Sulejmani

“…We present the first formal verification of approximation algorithms for NP-complete optimization problems: vertex cover, independent set, set cover, center selection, load balancing, and bin packing. …”
Get full text

Synthesis of a Controller Algorithm for Safety-Critical Systems by Fellipe Guilherme Rey de Souza, Celso Massaki Hirata, Simin Nadjm-Tehrani

“…For the design phase, STPA can be combined with SysML modeling activities, including simulation and formal verification of systems models to produce the control software more efficiently. …”
Get full text

Formal-Guided Fuzz Testing: Targeting Security Assurance From Specification to Implementation for 5G and Beyond by Jingda Yang, Sudhanshu Arya, Ying Wang

“…We design and implement formal verification to detect attack traces in critical protocols. …”
Get full text

The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier by Chlipala, Adam

“…We report on the design and implementation of an extensible programming language and its intrinsic support for formal verification. Our language is targeted at low-level programming of infrastructure like operating systems and runtime systems. …”
Get full text
Get full text

Shaded tangles for the design and verification of quantum programs by Reutter, D, Vicary, J

“…We analyze many known quantum programs in this way—including entanglement manipulation and error correction—and in each case present a fullytopological formal verification, yielding in several cases substantial new insight into how the program works. …”

Modeling Algorithms in SystemC and ACL2 by John W. O'Leary, David M. Russinoff

“…By means of a special-purpose parser, an algorithm coded in SystemC is converted to a MASC model for the purpose of documentation, which in turn is translated to ACL2 for formal verification. The parser also generates a SystemC variant that is suitable as input to a high-level synthesis tool. …”
Get full text

Implementation of the Composition-nominative Approach to Program Formalization in Mizar by Ievgen Ivanov, Artur Kornilowicz, Mykola Nikitchenko

“…The further aim of this work is development of a formal verification tool for software which processes and communicates with complex forms of data.…”
Get full text

Tool building requirements for an API to first-order solvers by Grundy, J, Melham, T, Krstić, S, McLaughlin, S

“…<p>Effective formal verification tools require that robust implementations of automatic procedures for first-order logic and satisfiability modulo theories be integrated into expressive interactive frameworks for logical deduction, such as higher-order logic theorem provers. …”

EVE: A tool for temporal equilibrium analysis by Gutierrez, J, Najib, M, Perelli, G, Wooldridge, M

“…We present EVE (Equilibrium Verification Environment), a formal verification tool for the automated analysis of temporal equilibrium properties of concurrent and multi-agent systems. …”

CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives by Kuepper, Joel, Erbsen, Andres, Gross, Jason, Conoly, Owen, Sun, Chuyue, Tian, Samuel, Wu, David, Chlipala, Adam, Chuengsatiansup, Chitchanok, Genkin, Daniel, Wagner, Markus, Yarom, Yuval

“…Some past work has shown how to do formal verification of that assembly, and other work has shown how to generate C code automatically along with formal proof, but with consequent performance penalties vs. the best- known assembly. …”
Get full text