Concept

Software verification

Publications associées (38)

On Verified Scala for STIX File System Embedded Code using Stainless

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

2022

Ontology-centric industrial requirements validation for aircraft assembly system design

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

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

TAYLOR & FRANCIS INC2020

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

2019

Learning Intelligent Dialogs for Bounding Box Annotation

Ksenia Konyushkova, Vittorio Ferrari

We introduce Intelligent Annotation Dialogs for bounding box annotation. We train an agent to automatically choose a sequence of actions for a human annotator to produce a bounding box in a minimal amount of time. Specifically, we consider two actions: box ...

IEEE2018

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

2017

Trustworthy Biometric Verification under Spoofing Attacks

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

Graph Chatbot

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

Connectez-vous pour utiliser Chat avec Graph Search