Abstract. Programming language technology can contribute to the development and understanding of Systems Biology by providing formal calculi for specifying and analysing the dynami...
Hanne Riis Nielson, Flemming Nielson, Henrik Pileg...
We describe data structures and algorithms for performing a path-sensitive program analysis to discover equivalences of expressions involving linear arithmetic or uninterpreted fun...
Role logic is a notation for describing properties of relational structures in shape analysis, databases and knowledge bases. A natural fragment of role logic corresponds to two-va...
We describe a polynomial-time algorithm for global value numbering, which is the problem of discovering equivalences among program sub-expressions. We treat all conditionals as non...
This paper addresses the verification of properties of imperative programs with recursive procedure calls, heap-allocated storage, and destructive updating of pointer-valued fiel...
Bertrand Jeannet, Alexey Loginov, Thomas W. Reps, ...
Abstract. The race condition checker rccjava uses a formal type system to statically identify potential race conditions in concurrent Java programs, but it requires programmer-supp...
hedron Abstract Domain Robert Claris´o and Jordi Cortadella Universitat Polit`ecnica de Catalunya Barcelona, Spain Abstract. An interesting area in static analysis is the study of...
Abstract. We specify an information flow analysis for a simple imperative language, using a Hoare-like logic. The logic facilitates static checking of a larger class of programs t...