Publications related to Model checking

A Formally Verified NAT

George Candea, Solal Vincenzo Pirelli, 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

Algorithmic Verification of Component-based Systems

Qiang Wang

This dissertation discusses algorithmic verification techniques for concurrent component-based systems modeled in the Behavior-Interaction-Priority (BIP) framework with both bounded and unbounded concurrency. BIP is a component framework for mixed software ...

EPFL2017

A methodology for the rigorous verification of Particle-in-Cell simulations

Paolo Ricci, Fabio Riva, Carrie Fiona Beadle

A methodology to perform a rigorous verification of Particle-in-Cell (PIC) simulations is presented, both for assessing the correct implementation of the model equations (code verification), and evaluating the numerical uncertainty affecting the simulation ...

American Institute of Physics2017

A methodology for the rigorous verification of plasma simulation codes

Paolo Ricci, Joaquim Loizu Cisquella, Paola Paruta, Sébastien Jolliet, Federico David Halpern, Fabio Riva, Annamaria Mosetto, Christoph Wersal, Carrie Fiona Beadle

A methodology to perform a rigorous verification of Particle-in-Cell (PIC) simulations is presented, both for assessing the correct implementation of the model equations (code verification), and evaluating the numerical uncertainty affecting the simulation ...

2017

Existence and Uniqueness of Load-Flow Solutions in Three-Phase Distribution Networks

Jean-Yves Le Boudec, Mario Paolone, Andrey Bernstein, Cong Wang

We present sufficient conditions for the existence and uniqueness of load-flow solutions in three-phase distribution networks. The conditions can be efficiently verified for real distribution systems. ...

Ieee-Inst Electrical Electronics Engineers Inc2017

Solving quantified linear arithmetic by counterexample-guided instantiation

Viktor Kuncak, Andrew Joseph Reynolds

This paper presents a framework to derive instantiation-based decision procedures for satisfiability of quantified formulas in first-order theories, including its correctness, implementation, and evaluation. Using this framework we derive decision procedur ...

2017

On verifying causal consistency

Rachid Guerraoui, Jad Hamza

Causal consistency is one of the most adopted consistency criteria for distributed implementations of data structures. It ensures that operations are executed at all sites according to their causal precedence. We address the issue of verifying automaticall ...

Robust Control Policies Given Formal Specifications in Uncertain Environments

Maryam Kamgarpour, Tony Alan Wood

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 ...

2017

NAND-NOR: A Compact, Fast, and Delay Balanced FPGA Logic Element

Paolo Ienne, Grace Zgheib, Yu Lin, Wei Li

The And-Inverter Cone has been introduced as an alternative logic element to the look-up table in FPGAs, since it improves their performance and resource utilization. However, further analysis of the AIC design showed that it suffers from the delay discrep ...

ACM2017

Parameterized Systems in BIP: Design and Model Checking

Joseph Sifakis, Simon Bliudze, Qiang Wang

BIP is a component-based framework for system design that has important industrial applications. BIP is built on three pillars: behavior, interaction, and priority. In this paper, we introduce first-order interaction logic (FOIL) that extends BIP to system ...

Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik2016

Model checking

A Formally Verified NAT

Algorithmic Verification of Component-based Systems

A methodology for the rigorous verification of Particle-in-Cell simulations

A methodology for the rigorous verification of plasma simulation codes

Existence and Uniqueness of Load-Flow Solutions in Three-Phase Distribution Networks

Solving quantified linear arithmetic by counterexample-guided instantiation

On verifying causal consistency

Robust Control Policies Given Formal Specifications in Uncertain Environments

NAND-NOR: A Compact, Fast, and Delay Balanced FPGA Logic Element

Parameterized Systems in BIP: Design and Model Checking

Graph Chatbot

Chat with Graph Search

Algorithmic Verification of Component-based Systems

A Formally Verified NAT

Robust Control Policies Given Formal Specifications in Uncertain Environments

Parameterized Systems in BIP: Design and Model Checking

Existence and Uniqueness of Load-Flow Solutions in Three-Phase Distribution Networks

A methodology for the rigorous verification of Particle-in-Cell simulations

A methodology for the rigorous verification of plasma simulation codes

Solving quantified linear arithmetic by counterexample-guided instantiation

On verifying causal consistency

NAND-NOR: A Compact, Fast, and Delay Balanced FPGA Logic Element