Concept

Assertion (software development)

Publications associées (10)

Automated Formal Verification of Software Network Functions

Formally verifying the correctness of software is necessary to merit the trust people put in software systems. Currently, formal verification requires human effort to prove that a piece of code matches its specification and code changes to improve verifiab ...

EPFL2024

User Guidance for Efficient Fact Checking

Quoc Viet Hung Nguyen, Thành Tâm Nguyên

The Web constitutes a valuable source of information. In recent years, it fostered the construction of large-scale knowledge bases, such as Freebase, YAGO, and DBpedia. The open nature of the Web, with content potentially being generated by everyone, howev ...

2019

User Guidance for Efficient Fact Checking

Thành Tâm Nguyên, Thanh Trung Huynh, Quoc Viet Hung Nguyen

ASSOC COMPUTING MACHINERY2019

Theory and Practice of Coroutines with Snapshots

Aleksandar Prokopec, Fengyun Liu

While event-driven programming is a widespread model for asynchronous computing, its inherent control flow fragmentation makes event-driven programs notoriously difficult to understand and maintain. Coroutines are a general control flow construct that can ...

2018

Analytical solutions to a coupled fluid dynamics and neutron transport problem with application to GeN-Foam verification

Konstantin Mikityuk

Code verification is an important part of software development process that asserts code correctness. In this work, analytical solutions are used in order to develop a simple multiphysics problem involving coupled fluid dynamics and neutron transport to be ...

2018

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

Programming with Specifications

Philippe Paul Henri Suter

This thesis explores the use of specifications for the construction of correct programs. We go beyond their standard use as run-time assertions, and present algorithms, techniques and implementations for the tasks of 1) program verification, 2) declarative ...

EPFL2012

Debug Determinism: The Sweet Spot for Replay-Based Debugging

George Candea, Cristian Zamfir

Deterministic replay tools offer a compelling approach to debugging hard-to-reproduce bugs. Recent work on relaxed-deterministic replay techniques shows that replay debugging with low in-production overhead is possible. However, despite considerable progre ...

2011

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

The Perfectly-Synchronized Round-based Model of Distributed Computing

Rachid Guerraoui, Bastian Pochon

The perfectly-synchronized round-based model provides the powerful abstraction of crash-stop failures with atomic and synchronous message delivery. This abstraction makes distributed programming very easy.We describe a technique to automatically transform ...

2007