Publications associées à Software verification

Ontology-centric industrial requirements validation for aircraft assembly system design

Dimitrios Kyritsis, Jinzhi Lu, Xiaochen Zheng

The development of an aircraft industrial system faces the challenge of integrative requirements validation with de-correlated modelling languages and distributed proprietary formats. This paper specifies an ontology-centric industrial requirements validat ...

ELSEVIER2022

Similarity conditions and cube model tests of snow drift and precipitation preferential deposition patterns

Michael Lehning, Borui Zhang, Qingwen Zhang

We explore the process of modeling aeolian snow transport around buildings by proposing a set of similarity requirements on simulating a single snow fall event with drifting. The similarity criteria are used to guide our wind tunnel tests from the particle ...

ELSEVIER2021

A Coarse-mesh Methodology for the Analysis of One and Two-phase Nuclear Reactor Thermal-hydraulics in a Multi-physics Context

Stefan Radman

The analysis of nuclear reactors for performance and safety assessment benefits from the use of computational tools. In this context, this work aims at the development and application of a thermal-hydraulics methodology and related software that respond to ...

EPFL2021

Verification of Software Network Functions with No Verification Expertise

Arseniy Zaostrovnykh

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

EPFL2020

Code Integration, Data Verification, and Models Validation Using the ITER Integrated Modeling and Analysis System (IMAS) in EUROfusion

Olivier Sauter, José Pedro Rebelo Ferreira Marques, Antoine Pierre Emmanuel Alexis Merle, Giovanni Tardini

The ITER Integrated Modelling and Analysis System (IMAS) has been adopted by the EUROfusion Consortium as a platform to facilitate the analysis and verification of data from multiple tokamaks for the integration of physics codes and the validation of physi ...

2020

Modeling of Simultaneous Propagation of Multiple Blade‑Like Hydraulic Fractures from a Horizontal Well

Brice Tanguy Alphonse Lecampion, Dmitry Nikolskiy

We explore different aspects of the multi-stage fracturing process such as stress interaction between growing hydraulic fractures, perforation friction, as well as the wellbore flow dynamics using a specifically developed numerical solver. In particular, g ...

2020

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

Trustworthy Biometric Verification under Spoofing Attacks : Application to the Face Mode

Ivana Chingovska

The need for automation of the identity recognition process for a vast number of applications resulted in great advancement of biometric systems in the recent years. Yet, many studies indicate that these systems suffer from vulnerabilities to spoofing (pre ...

EPFL2016

On recursion-free Horn clauses and Craig interpolation

Viktor Kuncak, Hossein Hojjat

One of the main challenges in software verification is efficient and precise analysis of programs with procedures and loops. Interpolation methods remain among the most promising techniques for such verification. To accommodate the demands of various progr ...

Springer2015

Building Evolvable Networks : Flexible and Predictable Packet Processing

Mihai Dobrescu

Software packet-processing platforms- - network devices running on general-purpose servers-- are emerging as a compelling alternative to the traditional high-end switches and routers running on specialized hardware. Their promise is to enable the fast dep ...

EPFL2015

Verification methodology for plasma simulations and application to a scrape-off layer turbulence code

Paolo Ricci, Sébastien Jolliet, Joaquim Loizu Cisquella, Federico David Halpern, Fabio Riva, Annamaria Mosetto

Bridging the gap between plasma physics and other scientific domains, in particular, the computational fluid dynamics community, a general, rigorous, and simple-to-apply methodology is presented for both the verification of the correct implementation of th ...

American Institute of Physics2014

Model Predictive-based Voltage Regulation of an Islanded Distributed Generation Unit

Alfred Rufer, Behrooz Bahrani

This paper presents a Discrete-time Model Predictive-based Control strategy for the voltage regulation of an islanded distributed generation (DG) unit. The DG unit includes a voltage source converter (VSC) interfaced to the grid through a switch and a coup ...

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

Decision Procedures for Program Synthesis and Verification

Ruzica Piskac

Decision procedures are widely used in software development and verification. The goal of this dissertation is to increase the scope of properties that can be verified using decision procedures. To achieve this goal, we identify three improvements over the ...

EPFL2011

Ordered Sets in the Calculus of Data Structures

Viktor Kuncak, Philippe Paul Henri Suter, Ruzica Piskac

Our goal is to identify families of relations that are useful for reasoning about software. We describe such families using decidable quantifier-free classes of logical constraints with a rich set of operations. A key challenge is to define such classes of ...

Springer2010

Software Verification by Combining Program Analyses of Adjustable Precision

Grégory Théoduloz

In automatic software verification, we have observed a theoretical convergence of model checking and program analysis. In practice, however, model checkers, on one hand, are still mostly concerned with precision, e.g., the removal of spurious counterexampl ...

EPFL2010

Runtime Checking for Separation Logic

Viktor Kuncak

Separation logic is a popular approach for specifying properties of recursive mutable data structures. Several existing systems verify a subclass of separation logic specifications using static analysis techniques. Checking data structure specifications du ...

Springer2008

Full Functional Verification of Linked Data Structures

Viktor Kuncak

We present the first verification of full functional correctness for a range of linked data structure implementations, including mutable lists, trees, graphs, and hash tables. Specifically, we present the use of the Jahob verification system to verify form ...

2008

Decision Procedures for Multisets with Cardinality Constraints

Viktor Kuncak, Ruzica Piskac

Applications in software verification and interactive theorem proving often involve reasoning about sets of objects. Cardinality constraints on such collections also arise in these scenarios. Multisets arise for analogous reasons as sets: abstracting the c ...

Springer2008