A First Step to the Categorical Logic of Quantum Programs by Xin Sun, Feifei He

“…The long-term goal of our research is to develop a powerful quantum logic which is useful in the formal verification of quantum programs and protocols. In this paper we introduce the basic idea of our categorical logic of quantum programs (CLQP): It combines the logic of quantum programming (LQP) and categorical quantum mechanics (CQM) such that the advantages of both LQP and CQM are preserved while their disadvantages are overcome. …”
Get full text

Run-Time Risk Mitigation in Automated Vehicles: A Model for Studying Preparatory Steps by Mario Gleirscher

“…By studying an example, this article investigates some achievements in the modeling for the steps (i), (ii), and (iii), amenable to formal verification of desired properties derived from potential assurance obligations such as the global existence of an effective mitigation strategy. …”
Get full text

Modeling and Verification of Infinite Systems with Resources by Martin Lang, Christof Löding

“…We consider formal verification of recursive programs with resource consumption. …”
Get full text

An Integrated Development Environment for the Prototype Verification System by Paolo Masci, César A. Muñoz

“…The steep learning curve of formal technologies is a well-known barrier to the adoption of formal verification tools in industry. This paper presents VSCode-PVS, a modern integrated development environment for the Prototype Verification System (PVS). …”
Get full text

Simultaneous task allocation and planning under uncertainty by Faruq, F, Lacerda, B, Hawes, N, Parker, D

“…Building upon techniques and tools from formal verification, we show how to generate a sequence of multi-robot policies, iteratively refining them to reallocate tasks if individual robots fail, and providing probabilistic guarantees on the performance (and safe operation) of the team of robots under the resulting policy. …”

Computing mutation coverage in interpolation-based model checking by Chockler, H, Kroening, D, Purandare, M

“…Coverage is a standard measure in testing, but is very difficult to compute in the context of formal verification. We present efficient algorithms for identifying those parts of the system that are covered by a given property. …”

Partial orders for efficient bounded model checking of concurrent software by Alglave, J, Kroening, D, Tautschnig, M

“…Modelling program executions with partial orders rather than interleavings addresses both issues: we obtain an efficient encoding into integer difference logic for bounded model checking that enables first-time formal verification of deployed concurrent systems code. …”

TRX: A Formally Verified Parser Interpreter by Adam Koprowski, Henri Binsztok

“…Parsing is an important problem in computer science and yet surprisingly little attention has been devoted to its formal verification. In this paper, we present TRX: a parser interpreter formally developed in the proof assistant Coq, capable of producing formally correct parsers. …”
Get full text

Using Model Checking for Analyzing Distributed Power Control Problems by Thomas Brihaye, Marc Jungers, Samson Lasaulce, Nicolas Markey, Ghassan Oreiby

“…Model checking (MC) is a formal verification technique which has been known and still knows a resounding success in the computer science community. …”
Get full text

A formalisation of XMAS by Bernard van Gastel, Julien Schmaltz

“…Communication fabrics play a key role in the correctness and performance of modern multi-core processors and systems-on-chip. To enable formal verification, a recent trend is to use high-level micro-architectural models to capture designers' intent about the communication and processing of messages. …”
Get full text

The Efficacy of Waste Management Plans in Australian Commercial Construction Refurbishment Projects by Mary Hardie, Shahed Khan, Angela O'Donnell, Graham Miller

“…Some reports indicate anabsence of any formal verification or monitoringprocess by regulators to assess the efficacy ofthe plans. …”
Get full text

A Specification Patterns System for Discrete Event Systems Analysis by Jose Creissac Campos, Jose Machado

“…As formal verification tools gain popularity, the problem arises of making them more accessible to engineers. …”
Get full text

Security and efficiency enhancement of an anonymous three-party password-authenticated key agreement using extended chaotic maps. by Qi Xie, Yanrong Lu, Xiao Tan, Zhixiong Tang, Bin Hu

“…Furthermore, we propose a novel scheme with enhanced security and efficiency. We use formal verification tool ProVerif, which is based on pi calculus, to prove security and authentication of our scheme. …”
Get full text

Formal Model Engineering for Embedded Systems Using Real-Time Maude by Peter Csaba Ölveczky

“…One can then use the code generation facilities of the tools for the modeling languages to automatically synthesize Real-Time Maude verification models from design models, enabling a formal model engineering process that combines the convenience of modeling using an informal but intuitive modeling language with formal verification. We give a brief overview six fairly different modeling formalisms for which Real-Time Maude has provided the formal semantics and (possibly) formal analysis. …”
Get full text

Using Model Checking for Analyzing Distributed Power Control Problems by Markey Nicolas, Jungers Marc, Lasaulce Samson, Oreiby Ghassan, Brihaye Thomas

“…<p/> <p>Model checking (MC) is a formal verification technique which has been known and still knows a resounding success in the computer science community. …”
Get full text

Automatic Verification of Critical Industrial Process with Automata by Luis E. Mendoza Morales

“…One way to achieve this goal is using formal verification techniques such as Model Checking (MC), which increases understanding of automated processes, revealing inconsistencies, ambiguities and incompleteness, which are not easily noticed. …”
Get full text

Formally Verifying a Programmable Network Switch by Liu, Jiazheng

“…In this thesis, we propose a novel formal-verification methodology aimed at establishing strong correctness theorems for synthesizable hardware designs for network functionality, demonstrated through a case-study analysis of a Tofino-like programmable switch that we call VeriSwit. …”
Get full text

An interpolating sequent calculus for quantifier-free Presburger arithmetic by Brillout, A, Kroening, D, Rümmer, P, al., E

“…Craig interpolation has become a versatile tool in formal verification, used for instance to generate program assertions that serve as candidates for loop invariants. …”

Quantitative verification of Kalman filters by Evangelidis, A, Parker, D

“…We propose novel formal verification techniques and software to perform a rigorous quantitative analysisof the effectiveness of Kalman filters. …”

Simultaneous task allocation and planning under uncertainty by Faruq, F, Lacerda, B, Hawes, N, Parker, D

“…Building upon techniques and tools from formal verification, we show how to generate a sequence of multi-robot policies, iteratively refining them to reallocate tasks if individual robots fail, and providing probabilistic guarantees on the performance (and safe operation) of the team of robots under the resulting policy. …”