| 2004 | A General Approach to Comparing Infinite-State Systems with Their Finite-State Specifications. Antonín Kucera, Philippe Schnoebelen |
| 2004 | A Higher Order Modal Fixed Point Logic. Mahesh Viswanathan, Ramesh Viswanathan |
| 2004 | A Semantics for Concurrent Separation Logic. Stephen D. Brookes |
| 2004 | A Survey of Regular Model Checking. Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson, Mayank Saksena |
| 2004 | A Symbolic Decision Procedure for Cryptographic Protocols with Time Stamps (Extended Abstract). Liana Bozga, Cristian Ene, Yassine Lakhnech |
| 2004 | An Extensional Spatial Logic for Mobile Processes. Daniel Hirschkoff |
| 2004 | Asynchronous Games 2: The True Concurrency of Innocence. Paul-André Melliès |
| 2004 | Basic Theory of Reduction Congruence forTwo Timed Asynchronous pi-Calculi. Martin Berger |
| 2004 | CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings Philippa Gardner, Nobuko Yoshida |
| 2004 | Characterizing EF and EX Tree Logics. Mikolaj Bojanczyk, Igor Walukiewicz |
| 2004 | Compiling Pattern Matching in Join-Patterns. Qin Ma, Luc Maranget |
| 2004 | Deciding Probabilistic Bisimilarity Over Infinite-State Probabilistic Systems. Tomás Brázdil, Antonín Kucera, Oldrich Strazovský |
| 2004 | Elimination of Quantifiers and Undecidability in Spatial Logics for Concurrency. Luís Caires, Étienne Lozes |
| 2004 | Extended Process Rewrite Systems: Expressiveness and Reachability. Mojmír Kretínský, Vojtech Rehák, Jan Strejcek |
| 2004 | Message-Passing Automata Are Expressively Equivalent to EMSO Logic. Benedikt Bollig, Martin Leucker |
| 2004 | Model Checking Restricted Sets of Timed Paths. Nicolas Markey, Jean-François Raskin |
| 2004 | Model Checking Timed Automata with One or Two Clocks. François Laroussinie, Nicolas Markey, Philippe Schnoebelen |
| 2004 | Modular Construction of Modal Logics. Corina Cîrstea, Dirk Pattinson |
| 2004 | On Flatness for 2-Dimensional Vector Addition Systems with States. Jérôme Leroux, Grégoire Sutre |
| 2004 | Open Maps, Alternating Simulations and Control Synthesis. Paulo Tabuada |
| 2004 | Parameterised Boolean Equation Systems (Extended Abstract). Jan Friso Groote, Tim A. C. Willemse |
| 2004 | Probabilistic Event Structures and Domains. Daniele Varacca, Hagen Völzer, Glynn Winskel |
| 2004 | Resource Control for Synchronous Cooperative Threads. Roberto M. Amadio, Silvano Dal-Zilio |
| 2004 | Resources, Concurrency and Local Reasoning. Peter W. O'Hearn |
| 2004 | Reversible Communicating Systems. Vincent Danos, Jean Krivine |
| 2004 | Session Types for Functional Multithreading. Vasco Thudichum Vasconcelos, António Ravara, Simon J. Gay |
| 2004 | Symbolic Bisimulation in the Spi Calculus. Johannes Borgström, Sébastien Briais, Uwe Nestmann |
| 2004 | The Pros and Cons of Netcharts. Nicolas Baudru, Rémi Morin |
| 2004 | Timed vs. Time-Triggered Automata. Pavel Krcál, Leonid Mokrushin, P. S. Thiagarajan, Wang Yi |
| 2004 | Type Based Discretionary Access Control. Michele Bugliesi, Dario Colazzo, Silvia Crafa |
| 2004 | Verification by Network Decomposition. Edmund M. Clarke, Muralidhar Talupur, Tayssir Touili, Helmut Veith |
| 2004 | Verifying Finite-State Graph Grammars: An Unfolding-Based Approach. Paolo Baldan, Andrea Corradini, Barbara König |
| 2004 | Zing: Exploiting Program Structure for Model Checking Concurrent Software. Tony Andrews, Shaz Qadeer, Sriram K. Rajamani, Yichen Xie |
| 2004 | µABC: A Minimal Aspect Calculus. Glenn Bruns, Radha Jagadeesan, Alan Jeffrey, James Riely |