5. FORMATS 2007: Salzburg, Austria

• Joost-Pieter Katoen:
  Abstraction of Probabilistic Systems. 1-3
  Electronic Edition (link) BibTeX
• Bruce H. Krogh:
  From Analysis to Design. 4
  Electronic Edition (link) BibTeX
• Franck Cassez:
  Efficient On-the-Fly Algorithms for Partially Observable Timed Games. 5-24
  Electronic Edition (link) BibTeX
• Sara Adams, Joël Ouaknine, James Worrell:
  Undecidability of Universality for Timed Automata with Minimal Resources. 25-37
  Electronic Edition (link) BibTeX
• Grégory Batt, Ramzi Ben Salah, Oded Maler:
  On Timed Models of Gene Networks. 38-52
  Electronic Edition (link) BibTeX
• Patricia Bouyer, Nicolas Markey:
  Costs Are Expensive! 53-68
  Electronic Edition (link) BibTeX
• Víctor A. Braberman, Jorge Lucángeli Obes, Alfredo Olivero, Fernando Schapachnik:
  Hypervolume Approximation in Timed Automata Model Checking. 69-81
  Electronic Edition (link) BibTeX
• Fabrice Chevalier, Deepak D'Souza, Pavithra Prabhakar:
  Counter-Free Input-Determined Timed Automata. 82-97
  Electronic Edition (link) BibTeX
• Pieter J. L. Cuijpers, Reinder J. Bril:
  Towards Budgeting in Real-Time Calculus: Deferrable Servers. 98-113
  Electronic Edition (link) BibTeX
• Henning Dierks, Sebastian Kupferschmid, Kim Guldstrand Larsen:
  Automatic Abstraction Refinement for Timed Automata. 114-129
  Electronic Edition (link) BibTeX
• Catalin Dima:
  Dynamical Properties of Timed Automata Revisited. 130-146
  Electronic Edition (link) BibTeX
• Georgios E. Fainekos, George J. Pappas:
  Robust Sampling for MITL Specifications. 147-162
  Electronic Edition (link) BibTeX
• Carlo A. Furia, Matteo Rossi:
  On the Expressiveness of MTL Variants over Dense Time. 163-178
  Electronic Edition (link) BibTeX
• Sergio Giro, Pedro R. D'Argenio:
  Quantitative Model Checking Revisited: Neither Decidable Nor Approximable. 179-194
  Electronic Edition (link) BibTeX
• Rodolfo Gómez, Howard Bowman:
  Efficient Detection of Zeno Runs in Timed Automata. 195-210
  Electronic Edition (link) BibTeX
• John Håkansson, Paul Pettersson:
  Partial Order Reduction for Verification of Real-Time Components. 211-226
  Electronic Edition (link) BibTeX
• Jan Jakob Jessen, Jacob Illum Rasmussen, Kim Guldstrand Larsen, Alexandre David:
  Guided Controller Synthesis for Climate Controller Using Uppaal Tiga. 227-240
  Electronic Edition (link) BibTeX
• Susmit Jha, Bryan A. Brady, Sanjit A. Seshia:
  Symbolic Reachability Analysis of Lazy Linear Hybrid Automata. 241-256
  Electronic Edition (link) BibTeX
• Minyoung Kim, Mark-Oliver Stehr, Carolyn L. Talcott, Nikil Dutt, Nalini Venkatasubramanian:
  Combining Formal Verification with Observed System Execution Behavior to Tune System Parameters. 257-273
  Electronic Edition (link) BibTeX
• Pavel Krcál, Martin Stigge, Wang Yi:
  Multi-processor Schedulability Analysis of Preemptive Real-Time Tasks with Variable Execution Times. 274-289
  Electronic Edition (link) BibTeX
• Paulo Nazareno Maia Sampaio, Laura Margarita Rodríguez Peralta, Jean-Pierre Courtiat:
  Designing Consistent Multimedia Documents: The RT-LOTOS Methodology. 290-303
  Electronic Edition (link) BibTeX
• Dejan Nickovic, Oded Maler:
  AMT: A Property-Based Monitoring Tool for Analog Systems. 304-319
  Electronic Edition (link) BibTeX
• Andreas Podelski, Silke Wagner:
  Region Stability Proofs for Hybrid Systems. 320-335
  Electronic Edition (link) BibTeX
• Anne Remke, Boudewijn R. Haverkort:
  CSL Model Checking Algorithms for Infinite-State Structured Markov Chains. 336-351
  Electronic Edition (link) BibTeX
• Farn Wang:
  Symbolic Simulation-Checking of Dense-Time Automata. 352-368
  Electronic Edition (link) BibTeX