Complementation, the inverse of the reduced product operation, is a technique for systemfinding minimal decompositions of abstract domains. Fil´e and Ranzato advanced the state ...
Enea Zaffanella, Patricia M. Hill, Roberto Bagnara
Programs represented in Static Single Assignment (SSA) form contain phi instructions (or functions) whose operational semantics are to merge values coming from distinct control flo...
Vugranam C. Sreedhar, Roy Dz-Ching Ju, David M. Gi...
ing Cryptographic Protocols with Tree Automata David Monniaux http://www.di.ens.fr/%7Fmonniaux, Laboratoire d’Informatique, ´Ecole Normale Sup´erieure, 45 rue d’Ulm , 75230 P...
Abstract. Binary Decision Graphs are an extension of Binary Decision Diagrams that can represent some infinite boolean functions. Three refinements of BDGs corresponding to class...
This paper describes a powerful method for dead code analysis and elimination in the presence of recursive data constructions. We describe partially dead recursive data using live...
The intrinsic complexity of most protocol speci cations in particular, and of asynchronous systems in general, lead us to study combinations of static analysis with classical model...
Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu
We define an operational semantics for the Signal language and design an analysis which allows to verify properties pertaining to the relation between values of the numeric and bo...
This paper presents and evaluates a set of analyses designed to reduce synchronization overhead in Java programs. Monitor-based synchronization in Java often causes significant ove...