Abstract: Vague or “fuzzy” concepts appear almost everywhere. The combination of fuzzy logic with logic programming op...

Abstract: We present a declarative language with a formal semantics for specifying both users’ privacy preferences and servi...

Abstract: Contents: We give a short survey on the following topics on verification of multithreaded programs: SPIN Specification i...

Abstract: The notion of approximate equivalence of programs plays a fundamental role in several fields of computer science. In par...

Abstract: Zero-knowledge proofs are two-party interactive protocols where one party (the prover) convinces the other one (the veri...

Abstract: Relational program logics allow reasoning about two programs or two runs of the same program. They provide an elegant me...

Abstract: In this talk we present a MySQL code generator for OCL expressions which is based on the use of stored procedures for ma...

Abstract: Implementors of abstract machines face complex, and often interacting, decisions regarding, e.g., data representation, i...

Abstract: “Shared resources” is the term we use to refer to the notation and companion methodology used to teach concu...

Abstract: Side-channel attacks break cryptosystems by exploiting information that is revealed by the system’s implementation...

Abstract: I introduce subsequence invariants, a new class of invariants for the specification and verification of concurrent syste...

Abstract: Separating data into lock-protected resources is an established paradigm of multi-threaded programming. Programs followi...

Abstract: Pure lambda calculus reduction strategies have been thoroughly studied, as they constitute the foundations of evaluation...

Abstract: Glass-box test data generation (TDG) is the process of automatically generating test input data for a program by conside...

Abstract: We consider the refinement of a static analysis method called thread-modular verification. It was an open question wheth...

Abstract: We present a development environment for automatically building smart, security-aware GUIs following a model-based appro...

Abstract: We apply the framework of abstract interpretation to derive an abstract semantic function for the modal μ-calculus. The ...

Abstract: Non-failure analysis aims at inferring that procedure calls in a program will never fail. This type of information has m...

Abstract: Constraint Handling Rules (CHR) is a concurrent committed-choice rule-based programming language introduced in the 1990s...

Abstract: Cryptography is decidable

Abstract: Formal verification of imperative programs provides a high guarantee of software reliability, but it is usually a human ...

Abstract: Service compositions define how serveral Web services (loosely coupled platform independent software components exposed ...

Abstract: Model-checking techniques suffer from the state explosion problem that prevents them to scale up. During the past decade...

Abstract: A difficult point when verifying heap manipulating programs is to be able to separate precisely the part of the heap tha...

Abstract: Regular Linear Temporal Logic (RLTL) is a temporal logic that extends the expressive power of Linear Temporal Logic (LTL...

Abstract: This is a followup to my previous talk on the topic. where I presented the basics of abstract interpretation and of para...

Abstract: Most systems based on separation logic consider only restricted forms of implication or non-separating conjunction, as f...

Abstract: Shared mutable objects pose challenges in reasoning, especially for data abstraction and modularity. We present a logic ...

Abstract: What to do when we have an empty slot in our popular Theory lunch series? Respond to the overwhelming popular demand for...