| 2004 | Type Based Discretionary Access Control. | Michele Bugliesi, Dario Colazzo, Silvia Crafa |
| 2004 | ABC: A Minimal Aspect Calculus. | Glenn Bruns, Radha Jagadeesan, Alan Jeffrey, James Riely |
| 2004 | A Semantics for Concurrent Separation Logic. | Stephen D. Brookes |
| 2004 | Deciding Probabilistic Bisimilarity Over Infinite-State Probabilistic Systems. | Toms Brzdil, Antonn Kucera, Oldrich Strazovsk |
| 2004 | A Symbolic Decision Procedure for Cryptographic Protocols with Time Stamps (Extended Abstract). | Liana Bozga, Cristian Ene, Yassine Lakhnech |
| 2004 | Symbolic Bisimulation in the Spi Calculus. | Johannes Borgstrm, Sbastien Briais, Uwe Nestmann |
| 2004 | Message-Passing Automata Are Expressively Equivalent to EMSO Logic. | Benedikt Bollig, Martin Leucker |
| 2004 | Characterizing EF and EX Tree Logics. | Mikolaj Bojanczyk, Igor Walukiewicz |
| 2004 | Basic Theory of Reduction Congruence forTwo Timed Asynchronous pi-Calculi. | Martin Berger |
| 2004 | The Pros and Cons of Netcharts. | Nicolas Baudru, Rmi Morin |
| 2004 | Verifying Finite-State Graph Grammars: An Unfolding-Based Approach. | Paolo Baldan, Andrea Corradini, Barbara Knig |
| 2004 | Zing: Exploiting Program Structure for Model Checking Concurrent Software. | Tony Andrews, Shaz Qadeer, Sriram K. Rajamani, Yichen Xie |
| 2004 | Resource Control for Synchronous Cooperative Threads. | Roberto M. Amadio, Silvano Dal-Zilio |
| 2004 | A Survey of Regular Model Checking. | Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson, Mayank Saksena |
| 2003 | Priority Rewrite Systems for OSOS Process Languages. | Irek Ulidowski |
| 2003 | Synthesis of Distributed Algorithms Using Asynchronous Automata. | Alin Stefanescu, Javier Esparza, Anca Muscholl |
| 2003 | A Process-Algebraic Language for Probabilistic I/O Automata. | Eugene W. Stark, Rance Cleaveland, Scott A. Smolka |
| 2003 | Equivalence Checking of Non-Flat Systems Is EXPTIME-hard. | Zdenek Sawa |
| 2003 | Quantitative Relations and Approximate Process Equivalences. | Alessandra Di Pierro, Chris Hankin, Herbert Wiklicky |
| 2003 | Full Abstraction for HOPLA. | Mikkel Nygaard, Glynn Winskel |
| 2003 | A Compositional Semantic Theory for Synchronous Component-based Design. | Barry Norton, Gerald Lttgen, Michael Mendler |
| 2003 | An Extension of Pushdown System and Its Model Checking Method. | Naoya Nitta, Hiroyuki Seki |
| 2003 | Modeling Consensus in a Process Calculus. | Uwe Nestmann, Rachele Fuzzati, Massimo Merro |
| 2003 | Netcharts: Bridging the gap between HMSCs and executable specifications. | Madhavan Mukund, K. Narayan Kumar, P. S. Thiagarajan |
| 2003 | Composition of Cryptographic Protocols in a Probabilistic Polynomial-Time Process Calculus. | Paulo Mateus, John C. Mitchell, Andre Scedrov |