Stepwise Refinement of Formal Specifications Based on Logical Formulae: from COOPN/2 Specifications to Java Programs
Graph Chatbot
Chat with Graph Search
Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.
DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.
We present an approach for using formal methods in embedded systems and its evaluation on a case study. In our approach, the developers describe the system in a restricted subset of the high-level programming language Scala. We then use 1) a verification s ...
This semester project report describes a prototype tracing tool that records the behavior of a Java program during its execution. It explains the two methods that were attempted to implement the tool, one using the Java debug interface, which gave poor res ...
Writing correct software is hard, yet in systems that have a high failure cost or are not easily upgraded like blockchains, bugs and security problems cannot be tolerated. Therefore, these systems are perfect use cases for formal verification, the task of ...
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 de ...
In hard real-time embedded systems, design and specification methods and their associated tools must allow development of temporally deterministic systems to ensure their safety. To achieve this goal, we are specifically interested in methodologies based o ...
Programming languages are increasingly compiled to multiple runtimes, each featuring their own rich structures such as their object model.
Furthermore, they need to interact with other languages targeting said runtimes.
A language targeting only one runtim ...
Software network functions (NFs), such as a network address translator, load balancer, or proxy,
promise to bring flexibility and rapid innovation to computer networks and to reduce operational costs.
However, continuous updates and flexibility typically c ...
We present a trustworthy connection between the Leon verification system and the Isabelle proof assistant. Leon is a system for verifying functional Scala programs. It uses a variety of automated theorem provers (ATPs) to check verification conditions (VCs ...
We consider robust control synthesis for linear systems with complex specifications that are affected by uncertain disturbances. This letter is motivated by autonomous systems interacting with partially known, time-varying environments. Given a specificati ...
The fast widening of biosensing applications, such as healthcare, drug delivery, food, and military industries, is increasing the need for generality and compatibility among different sensors. To address this challenge, we present here an innovative approa ...
