Formal verification

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code. The verification of these systems is done by providing a formal proof on an abstract mathematical model of the system, the correspondence between the mathematical model and the nature of the system being otherwise known by construction. Examples of mathematical objects often used to model systems are: finite-state machines, labelled transition systems, Petri nets, vector addition systems, timed automata, hybrid automata, process algebra, formal semantics of programming languages such as operational semantics, denotational

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related publications (62)

Related publications

Related people (10)

Related people

Related units (7)

Related units

Related concepts (44)

Related concepts

Related courses (24)

Related courses

Related lectures (36)

Related lectures

Supporting Loop Proofs in KeY by using BLAST

Mathias Krebs

In contrast to beta-testing, formal verification can guarantee correctness of a program against a specification. Two basic verification techniques are theorem proving and model checking. Both have strengths and weaknesses. Theorem proving is powerful, but difficult to use for a software engineer. Model checking is fully automatic, but less powerful and hard to extend. This paper shows a possibility, how to combine both approaches, in order to surround the weaknesses. Concretely, we automatize the proof of while loops in the theorem prover KeY, by using the model checker BLAST.

2006

Extending Safe C Support In Leon

Marco Adriano Antognini

As hardware designs get more robust and efficient, software can solve a wider range of challenges, each one more advanced than the previous one. The direct consequence is that software complexity grows continuously. Despite being used more frequently in development processes, traditional testing frameworks are not enough to avoid flaws in programs. Moreover, many company concerned by the security of their applications, especially in mission critical industries, spend a considerable effort and amount of money to write robust software certified by solid guidelines and standards. For embedded systems, MISRA C is a certification process commonly used which provides directives to write portable and maintainable C code while avoiding many pitfalls of the language. Leon takes an orthogonal approach by providing tools for formal verification of programs written in a subset of Scala. In a previous work we introduced GenC, a module for Leon that converts Scala applications into equivalent and safe C99 programs, allowing developers to leverage high-level feature of Scala to implement robust applications, even for embedded systems. The aim of this project is to augment Leon and GenC in order to support a larger fragment of Scala that includes inheritance, generic programming, additional numeric types, pattern matching and more. Additionally, we closely analyse the MISRA Guidelines and shape the generated C code to work towards compliance with its rules while taking advantage of the verification capabilities of Leon to automatically detect a variety of bugs. We discuss these improvements and new features by implementing the famous LZW compression/decompression algorithm as well as a kernel-based image processing algorithm and show that the produced native C programs are significantly more efficient both in terms of memory usage but also in terms of execution speed.

2017

A Simpler and Faster NIC Driver Model for Network Functions

George Candea, Solal Vincenzo Pirelli

The advent of software network functions calls for stronger correctness guarantees and higher performance at every level of the stack. Current network stacks trade simplicity for performance and flexibility, especially in their driver model. We show that performance and simplicity can coexist, at the cost of some flexibility, with a new NIC driver model tailored to network functions. The key idea behind our model is that the driver can efficiently reuse packet buffers because buffers follow a single logical path. We implement a driver for the Intel 82599 network card in 550 lines of code. By merely replacing the state-of-theart driver with our driver, formal verification of the entire software stack completes in 7x less time, while the verified functions’ throughput improves by 160%. Our driver also beats, on realistic workloads, the throughput of drivers that cannot yet be formally verified, thanks to its low variability and resource use. Our code is available at github.com/dslab-epfl/tinynf.

2021

Computer science

Computer science is the study of computation, information, and automation. Computer science spans theoretical disciplines (such as algorithms, theory of computation, and information theory) to applied

Model checking

In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically a

Automated theorem proving

Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Autom

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to use formal verification tools and explain the theory and the practice behind them.

CS-320: Computer language processing

We teach the fundamental aspects of analyzing and interpreting computer languages, including the techniques to build compilers. You will build a working compiler from an elegant functional language into the new web standard for portable binaries called WebAssembly ( https://webassembly.org/ )

MATH-203(b): Analysis III

Le cours étudie les concepts fondamentaux de l'analyse vectorielle et l'analyse de Fourier en vue de leur utilisation pour résoudre des problèmes pluridisciplinaires d'ingénierie scientifique.