Concept

Hoare logic

Related publications (8)

Automated Formal Verification of Software Network Functions

Formally verifying the correctness of software is necessary to merit the trust people put in software systems. Currently, formal verification requires human effort to prove that a piece of code matches its specification and code changes to improve verifiab ...

EPFL2024

On algebraic array theories

Viktor Kuncak, Rodrigo Raya

Automatic verification of programs manipulating arrays relies on specialised decision procedures. A methodology to classify the theories handled by these procedures is introduced. It is based on decomposition theorems in the style of Feferman and Vaught. T ...

Elsevier Science Inc2023

A Formally Verified NAT

George Candea, Solal Vincenzo Pirelli, Aikaterini Argyraki, Arseniy Zaostrovnykh, Luis David Figueiredo Mascarenhas Moreira Pedrosa

We present a Network Address Translator (NAT) written in C and proven to be semantically correct according to RFC 3022, as well as crash-free and memory-safe. There exists a lot of recent work on network verification, but it mostly assumes models of networ ...

Assoc Computing Machinery2017

Deciding Conditional Termination

We address the problem of conditional termination, which is that of defining the set of initial configurations from which a given program always terminates. First we define the dual set, of initial configurations from which a non-terminating execution exis ...

Tech Univ Braunschweig2014

ScalaDyno: Making Name Resolution and Type Checking Fault-tolerant

Martin Odersky, Vlad Ureche, Cédric Bastin

The ScalaDyno compiler plugin allows fast prototyping with the Scala programming language, in a way that combines the benefits of both statically and dynamically typed languages. Static name resolution and type checking prevent partially-correct code from ...

ACM2014

Proving non-termination

Andrey Rybalchenko, Ashutosh Kumar Gupta

The search for proof and the search for counterexamples (bugs) are complementary activities that need to be pursued concurrently in order to maximize the practical success rate of verification tools. While this is well-understood in safety verification, th ...

2008

How to specify and how to prove correctness of secure routing protocols for MANET

Jean-Pierre Hubaux, Panagiotis Papadimitratos

Secure routing protocols for mobile ad hoc networks have been developed recently yet, it has been unclear what are the properties they achieve, as a formal analysis of these protocols is mostly lacking. In this paper we are concerned with this problem, how ...

Ieee Service Center, 445 Hoes Lane, Po Box 1331, Piscataway, Nj 08855-1331 Usa2006

How to Specify and How to Prove Correctness of Secure Routing Protocols for MANET

Jean-Pierre Hubaux, Panagiotis Papadimitratos

Secure routing protocols for mobile ad hoc networks have been developed recently, yet, it has been unclear what are the properties they achieve, as a formal analysis of these protocols is mostly lacking. In this paper, we are concerned with this problem, h ...

2006