Publication

Exploiting Various Levels of Semantics in CO-OPN for the SANDS Environment Tools

Publications associées (58)

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

Extended Connectors: Structuring Glue Operators in BIP

Simon Bliudze, Eduard Baranov

Based on a variation of the BIP operational semantics using the offer predicate introduced in our previous work, we extend the algebras used to model glue operators in BIP to encompass priorities. This extension uses the Algebra of Causal Interaction Trees ...

2013

STM in the Small: Trading Generality for Performance in Software Transactional Memory

Aleksandar Dragojevic

Data structures implemented using software transactional memory (STM) have a reputation for being much slower than data structures implemented directly from low-level primitives such as atomic compare-and-swap (CAS). In this paper we present a specialized ...

2012

Towards Complete Reasoning about Axiomatic Specifications

Viktor Kuncak, Swen Jacobs

To support verification of expressive properties of functional programs, we consider algebraic style specifications that may relate multiple user-defined functions, and compare multiple invocations of a function for different arguments. We present decision ...

Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa2011

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

Shape Refinement through Explicit Heap Analysis

Dirk Thilo Beyer, Grégory Théoduloz, Damien Zufferey

Shape analysis is a promising technique to prove program properties about recursive data structures. The challenge is to automatically determine the data-structure type, and to supply the shape analysis with the necessary information about the data structu ...

Springer2010

On Satisfiability Modulo Computable Functions

Viktor Kuncak, Philippe Paul Henri Suter, Ali Sinan Köksal

We present a semi-decision procedure for checking satisfiability of formulas in the language of algebraic data types and integer linear arithmetic extended with user-defined terminating recursive functions. Our procedure is designed to integrate into a DPL ...

2010

Decision Procedures for Algebraic Data Types with Abstractions

Viktor Kuncak, Philippe Paul Henri Suter, Mirco Dotta

We describe a family of decision procedures that extend the decision procedure for quantifier-free constraints on recursive algebraic data types (term algebras) to support recursive abstraction functions. Our abstraction functions are catamorphisms (term a ...

2010

Building a Calculus of Data Structures

Viktor Kuncak, Philippe Paul Henri Suter, Ruzica Piskac

Techniques such as verification condition generation, predicate abstraction, and expressive type systems reduce software verification to proving formulas in expressive logics. Programs and their specifications often make use of data structures such as sets ...

Springer2010

Formalizing and verifying transactional memories

Vasu Singh

Transactional memory (TM) has shown potential to simplify the task of writing concurrent programs. TM shifts the burden of managing concurrency from the programmer to the TM algorithm. The correctness of TM algorithms is generally proved manually. The goal ...

EPFL2010

Routing Attacks as a Viable Threat: Can Software Systems Protect Themselves?

Dan Alistarh

In this paper, we show that distributed systems are vul- nerable to routing attacks and propose an architecture to obviate this vulnerability. A somewhat surprising finding is that even a small-scale routing attack can completely dis- rupt the operation of ...

2010