Journal: Electronic Notes in Theoretical Computer Science

Volume 190, Issue 4

1 -- 2Sabine Glesner, Jens Knoop, Rolf Drechsler. Preface
3 -- 16Roderick Bloem, Stefan Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli, Martin Weiglhofer. Specify, Compile, Run: Hardware from PSL
17 -- 32G. W. Hamilton. Distilling Programs for Verification
33 -- 48María-del-Mar Gallardo, Christophe Joubert, Pedro Merino. On-the-Fly Data Flow Analysis Based on Verification Technology
49 -- 63Ling Fang, Masataka Sassa. Generating Java Compiler Optimizers Using Bidirectional CTL
65 -- 82Jan Olaf Blech, Arnd Poetzsch-Heffter. A Certifying Code Generation Phase

Volume 190, Issue 3

1 -- 2Alessandro Aldini, Franck van Breugel. Preface
3 -- 25Ashok Argent-Katwala, Jeremy T. Bradley. PEPA Queues: Capturing Customer Behaviour in Queueing Networks
27 -- 42Luca Bortolussi, Alberto Policriti. Stochastic Concurrent Constraint Programming and Differential Equations
43 -- 58Vincenzo Ciancia, Gian Luigi Ferrari. Co-Algebraic Models for Quantitative Spatial Logics
59 -- 77Alessandra Di Pierro, Chris Hankin, Herbert Wiklicky. On Probabilistic Techniques for Data Flow Analysis
79 -- 94Tom Chothia, Jun Pang, Muhammad Torabi Dashti. Keeping Secrets in Resource Aware Components
95 -- 110Pedro Baltazar, Paulo Mateus, Rajagopal Nagarajan, Nikolaos Papanikolaou. Exogenous Probabilistic Computation Tree Logic
111 -- 127Stefano Bistarelli, Ugo Montanari, Francesca Rossi, Francesco Santini. Modelling Multicast QoS Routing by using Best-Tree Search in And-or Graphs and Soft Constraint Logic Programming
129 -- 145Michael J. A. Smith. Stochastic Modelling of Communication Protocols from Source Code
147 -- 166Daniele Varacca, Nobuko Yoshida. Probabilistic pi-Calculus and Event Structures
167 -- 183Gagarine Yaikhom, Murray Cole, Stephen Gilmore, Jane Hillston. A Structural Approach for Modelling Performance of Systems Using Skeletons
185 -- 203Yuxin Deng, Wenjie Du. Probabilistic Barbed Congruence

Volume 190, Issue 2

1 -- 0Bernd Finkbeiner, Yuri Gurevich, Alexander K. Petrenko. Preface
3 -- 19Sergiy Boroday, Alexandre Petrenko, Roland Groz. Can a Model Checker Generate Tests for Non-Deterministic Systems?
21 -- 32Frédéric Dadeau, Yves Ledru, Lydie du Bousquet. Measuring a Java Test Suite Coverage Using JML Specifications
33 -- 46Gordon Fraser, Bernhard K. Aichernig, Franz Wotawa. Handling Model Changes: Regression Testing and Test-Suite Update with Model-Checkers
47 -- 59Anders Hessel, Paul Pettersson. A Global Algorithm for Model-Based Test Suite Generation
61 -- 72Maik Kollmann, Yuen Man Hon. Generating Scenarios by Multi-Object Checking
73 -- 84Yves Ledru, Lydie du Bousquet, Frédéric Dadeau, F. Allouti. A Case Study in Matching Test and Proof Coverage
85 -- 97Martin Ouimet, Kristina Lundqvist. Automated Verification of Completeness and Consistency of Abstract State Machine Specifications using a SAT Solver
99 -- 111Ana Paiva, João C. P. Faria, Raul F. A. M. Vidal. Towards the Integration of Visual and Formal Models for GUI Testing
113 -- 125Franco Raimondi, Charles Pecheur, Guillaume Brat. Testing Planning Domains (without Model Checkers)

Volume 190, Issue 1

1 -- 0Marieke Huisman, Fausto Spoto. Preface
3 -- 18Jesse McGeachie, Jürgen Dingel. Translate One, Analyze Many: Leveraging the Microsoft Intermediate Language and Source Code Transformation for Model Checking
19 -- 33Emilie Balland, Pierre-Etienne Moreau, Antoine Reilles. Bytecode Rewriting in Tom
35 -- 50Hermann Lehner, Peter Müller. Formal Translation of Bytecode into BoogiePL
51 -- 66Mario Méndez-Lojo, Jorge Navas, Manuel V. Hermenegildo. An Efficient, Parametric Fixpoint Algorithm for Analysis of Java Bytecode
67 -- 83Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla, Damiano Zanardini. Experiments in Cost Analysis of Java Bytecode
85 -- 101Miguel Gómez-Zamalloa, Elvira Albert, Germán Puebla. Improving the Decompilation of Java Bytecode to Prolog by Partial Evaluation
103 -- 119Ando Saabas, Tarmo Uustalu. Type Systems for Optimizing Stack-based Code
121 -- 132Quan Hoang Nguyen, Bernhard Scholz. Computing SSA Form with Matrices
133 -- 147Jaroslav Sevcík. Proving Resource Consumption of Low-level Programs Using Automated Theorem Provers
149 -- 160Theo C. Ruys, Niels H. M. Aan de Brugh. MMC: the Mono Model Checker