Last update: Thu Aug 29 06:18:57 MDT 2024
Volume 1, Number 1--2, December, 1997W. Rance Cleaveland and Tiziana Margaria and Bernhard Steffen Editorial . . . . . . . . . . . . . . . 1--5 Pierre Wolper The meaning of ``formal'': from weak to strong formal methods . . . . . . . . . 6--8 Bernhard Steffen and Tiziana Margaria and Volker Braun The Electronic Tool Integration platform: concepts and design . . . . . 9--30 Volker Braun and Tiziana Margaria and Carsten Weise Integrating tools in the ETI platform 31--48 Tiziana Margaria and Volker Braun and Jürgen Kreileder Interacting with ETI: a user session . . 49--63 Kim G. Larsen and B. Steffen and C. Weise Continuous modeling of real-time and hybrid systems: from concepts to tools 64--85 Rajeev Alur and Thomas A. Real-time system = discrete system + clock variables . . . . . . . . . . . . 86--109 Thomas A. Henzinger and Pei-Hsin Ho and Howard Wong-Toi HYTECH: a model checker for hybrid systems . . . . . . . . . . . . . . . . 110--122 Sergio Yovine KRONOS: a verification tool for real-time systems . . . . . . . . . . . 123--133 Kim G. Larsen and Paul Pettersson and Wang Yi Uppaal in a nutshell . . . . . . . . . . 134--152 Philippe Leblanc OMT and SDL based techniques and tools for design, simulation and test production of distributed systems . . . 153--165 Marius Bozga and Jean-Claude Fernandez and Alain Kerbrat and Laurent Mounier Protocol verification with the ALDÉBARAN toolset . . . . . . . . . . . . . . . . 166--183
Gregor Snelting Paul Feyerabend and software technology 1--5 Chris Hankin Program analysis tools . . . . . . . . . 6--12 Torben Amtoft and Hanne Riis Nielson and Flemming Nielson Behavior analysis for validating communication patterns . . . . . . . . . 13--28 Michael Codish and Bart Demoen and Konstantinos Sagonas Semantics-based program analysis for logic-based languages using XSB . . . . 29--45 Florian Martin PAG --- an efficient program analyzer generator . . . . . . . . . . . . . . . 46--67 Mihaela Sighireanu and Radu Mateescu Verification of the Link layer protocol of the IEEE-1394 serial bus (FireWire): an experiment with E-LOTOS . . . . . . . 68--88
Perdita Stevens A verification tool developer's vade mecum . . . . . . . . . . . . . . . . . 89--94 Kurt Jensen Preface by the Section Editor: Kurt Jensen . . . . . . . . . . . . . . . . . 95--97 Lars M. Kristensen and Soren Christensen and Kurt Jensen The practitioner's guide to coloured Petri nets . . . . . . . . . . . . . . . 98--132 Jianli Xu and Juha Kuusela Analyzing the execution architecture of mobile phone software with colored Petri nets . . . . . . . . . . . . . . . . . . 133--143 Steven Gordon and Jonathan Billington Analysing a missile simulator with coloured Petri nets . . . . . . . . . . 144--159 Gilles Moncelet and Sòren Christensen and Hamid Demmou and Mario Paludetto and José Porras Analysing a mechatronic system with coloured Petri nets . . . . . . . . . . 160--167 Lee W. Wagenhals and Insub Shin and Alexander H. Levis Creating executable models of influence nets with colored Petri nets . . . . . . 168--181 F. P. Burns and A. M. Koelmans and A. V. Yakovlev Analysing superscalar processor architectures with coloured Petri nets 182--191 A. Pnueli and O. Shtrichman and M. Siegel The Code Validation Tool (CVT): Automatic verification of a compilation process . . . . . . . . . . . . . . . . 192--201 Thomas Friese and Tiziana Margaria and Alfred Hofmann Integrating printed and online information . . . . . . . . . . . . . . 202--202
Steven D. Johnson A workshop on formal methods education: held at Melbourne Florida in March 1998 [5]: an aggregation of opinions . . . . 203--207 Rance Cleaveland Pragmatics of model checking: an STTT special section . . . . . . . . . . . . 208--218 Xiaoqun Du and Scott A. Smolka and Rance Cleaveland Local model checking and protocol analysis . . . . . . . . . . . . . . . . 219--241 Henrik Reif Andersen and Jorn Lind-Nielsen Partial model checking of modal equations: a survey . . . . . . . . . . 242--259 Sérgio Vale Aguiar Campos and Edmund Clarke Analysis and verification of real-time systems using quantitative symbolic algorithms . . . . . . . . . . . . . . . 260--269 Gerard J. Holzmann and Anuj Puri A minimized automaton representation of reachable states . . . . . . . . . . . . 270--278 E. M. Clarke and O. Grumberg and M. Minea and D. Peled State space reduction using partial order techniques . . . . . . . . . . . . 279--287 Carl Pixley and Vigyan Singhal Model checking: a hardware design perspective . . . . . . . . . . . . . . 288--306 C. Barry Jay Programming in FISh . . . . . . . . . . 307--315
George S. Avrunin and James C. Corbett and Matthew B. Dwyer Benchmarking finite-state verifiers . . 317--320 Gerard Holzmann and Eli Najm and Ahmed Serhrouchni SPIN model checking: an introduction . . 321--327 Yonit Kesten and Amir Pnueli Control and data abstraction: the cornerstones of practical formal verification . . . . . . . . . . . . . . 328--342 Lynette I. Millett and Tim Teitelbaum Issues in slicing PROMELA and its applications to model checking, protocol understanding, and simulation . . . . . 343--349 Willem Visser and Howard Barringer Practical CTL$^*$ model checking: Should SPIN be extended? . . . . . . . . . . . 350--365 Klaus Havelund and Thomas Pressburger Model checking JAVA programs using JAVA PathFinder . . . . . . . . . . . . . . . 366--381 René G. de Vries and Jan Tretmans On-the-fly conformance testing using SPIN . . . . . . . . . . . . . . . . . . 382--393 Moataz Kamel and Stefan Leue Formalization and validation of the General Inter-ORB Protocol (GIOP) using PROMELA and SPIN . . . . . . . . . . . . 394--409 Alessandro Cimatti and Edmund Clarke and Fausto Giunchiglia and Marco Roveri NUSMV: a new symbolic model checker . . 410--425
Fausto Giunchiglia and Paolo Traverso Theorem proving in technology transfer: the user's point of view . . . . . . . . 1--12 Matt Kaufmann Verification of Year 2000 conversion rules using the ACL2 theorem prover . . 13--19 Ben L. Di Vito High-automation proofs for properties of requirements models . . . . . . . . . . 20--31 Deepak Kapur and Mahadevan Subramaniam Using an induction prover for verifying arithmetic circuits . . . . . . . . . . 32--65 Serge Autexier and Dieter Hutter and Bruno Langenstein and Heiko Mantel and Georg Rock and Axel Schairer and Werner Stephan and Roland Vogt and Andreas Wolpers VSE: formal methods meet industrial needs . . . . . . . . . . . . . . . . . 66--77 Paolo Traverso and Piergiorgio Bertoli Mechanized result verification: an industrial application . . . . . . . . . 78--92 Alexander Aiken and Manuel Fähndrich and Zhendong Su Detecting races in Relay Ladder Logic programs . . . . . . . . . . . . . . . . 93--105
Ed Brinksma Verification is experimentation! . . . . 107--111 Rolf Drechsler and Detlef Sieling Binary decision diagrams in theory and practice . . . . . . . . . . . . . . . . 112--136 Randal E. Bryant and Yirng-An Chen Verification of arithmetic circuits using binary moment diagrams . . . . . . 137--155 Shin-ichi Minato Zero-suppressed BDDs and their applications . . . . . . . . . . . . . . 156--170 Fabio Somenzi Efficient manipulation of decision diagrams . . . . . . . . . . . . . . . . 171--181 Stefan Höreth A word-level graph manipulation package 182--192 Justin E. Harlow III and Franc Brglez Design of experiments and evaluation of BDD ordering heuristics . . . . . . . . 193--206 Janett Mohnke and Paul Molitor and Sharad Malik Application of BDDs in Boolean matching techniques for formal logic combinational verification . . . . . . . 207--216 Berna L. Massingill and Timothy G. Mattson and Beverly A. Sanders Parallel programming with a pattern language $^*$ . . . . . . . . . . . . . 217--234 Alberto Bartoli and Gianluca Dini and Lanfranco Lopriore Application-controlled memory management in a single address space environment 235--245
Rance Cleaveland Preface by the section editor . . . . . 247--249 Giorgio Delzanno and Andreas Podelski Constraint-based deductive model checking . . . . . . . . . . . . . . . . 250--270 Daniel Hirschkoff Bisimulation verification using the up to techniques . . . . . . . . . . . . . 271--285 Christoph Kern and Tarik Ono-Tesfaye and Mark R. Greenstreet A light-weight framework for hardware verification . . . . . . . . . . . . . . 286--313 Hubert Garavel and César Viho and Massimo Zendri System design of a CC-NUMA multiprocessor architecture using formal specification, model-checking, co-simulation, and test generation . . . 314--331 Marieke Huisman and Bart Jacobs and Joachim van den Berg A case study in class library verification: Java's vector class . . . 332--352 Magnus Lindahl and Paul Pettersson and Wang Yi Formal design and analysis of a gear controller . . . . . . . . . . . . . . . 353--368
Kurt Jensen Preface by the section editor . . . . . 369--371 Gérard Berthelot and Laure Petrucci Specification and validation of a concurrent system: an educational project . . . . . . . . . . . . . . . . 372--381 Leo Ojala and Nisse Husberg and Teemu Tynjälä Modelling and analysing a distributed dynamic channel allocation algorithm for mobile computing using high-level net methods . . . . . . . . . . . . . . . . 382--393 Hartmann Genrich and Robert Küffner and Klaus Voss Executable Petri net models for the analysis of metabolic pathways . . . . . 394--404 Bo Lindstrom Web-based interfaces for simulation of coloured Petri net models . . . . . . . 405--416 S. Bernardi and S. Donatelli and A. Horváth Implementing compositionality for stochastic Petri nets . . . . . . . . . 417--430 Matthias Anlauff and Samarjit Chakraborty and Philipp W. Kutter and Alfonso Pierantonio and Lothar Thiele Generating an action notation environment from Montages descriptions 431--455 Alex Aizman Easy concurrency . . . . . . . . . . . . 456--468 David P. L. Simons and Mariëlle I. A. Stoelinga Mechanical verification of the IEEE 1394a root contention protocol using Uppaal2k . . . . . . . . . . . . . . . . 469--485 Ekkart Kindler and Michael Weber The Petri Net Kernel: an infrastructure for building Petri net tools . . . . . . 486--497
Mary Shaw What makes good research in software engineering? . . . . . . . . . . . . . . 1--7 Klaus Havelund and Willem Visser Program model checking as a new trend 8--20 Ed Brinksma and Angelika Mader and Ansgar Fehnker Verification and optimization of a PLC control schedule . . . . . . . . . . . . 21--33 James C. Corbett and Matthew B. Dwyer and John Hatcliff and Robby Expressing checkable properties of dynamic systems: the Bandera Specification Language . . . . . . . . . 34--56 Heikki Tauriainen and Keijo Heljanko Testing LTL formula translation into Büchi automata . . . . . . . . . . . . . 57--70 Scott D. Stoller Model-checking multi-threaded distributed Java programs . . . . . . . 71--91 Dragan Bo\vsna\vcki and Dennis Dams and Leszek Holenderski Symmetric Spin . . . . . . . . . . . . . 92--106 Cindy Eisner Using symbolic CTL model checking to verify the railway stations of Hoorn-Kersenboogerd and Heerhugowaard 107--124 E. M. Clarke and M. Fujita and S. P. Rajan and T. Reps and S. Shankar and T. Teitelbaum Program slicing for VHDL . . . . . . . . 125--137
Susanne Graf Preface by the section editor . . . . . 139--141 Marius Bozga and Jean-Claude Fernandez and Lucian Ghirvu Using static analysis to improve automatic test generation . . . . . . . 142--152 Holger Hermanns and Joost-Pieter Katoen and Joachim Meyer-Kayser and Markus Siegle A tool for model-checking Markov chains 153--172 Edmund Clarke and Somesh Jha and Will Marrero Efficient verification of security protocols using partial-order reductions 173--188 Louise A. Dennis and Graham Collins and Michael Norrish and Richard J. Boulton and Konrad Slind and Thomas F. Melham The PROSPER toolkit . . . . . . . . . . 189--210 Steven D. Johnson and Yanhong A. Liu and Yuchen Zhang A systematic incrementalization technique and its application to hardware design . . . . . . . . . . . . 211--223 Orna Kupferman and Moshe Y. Vardi Vacuity detection in temporal model checking . . . . . . . . . . . . . . . . 224--233 Hong Peng and Sofi\`ene Tahar and Ferhat Khendek Comparison of SPIN and VIS for protocol verification . . . . . . . . . . . . . . 234--245 Theo C. Ruys and Ed Brinksma Managing the verification trajectory . . 246--259
Jeannette M. Wing Platitudes and attitudes . . . . . . . . 261--265 Tiziana Margaria Preface by the section editor . . . . . 266--270 Alan Mycroft and Richard Sharp Higher-level techniques for hardware description and synthesis . . . . . . . 271--297 Mark D. Aagaard and Byron Cook and Nancy A. Day and Robert B. Jones A framework for superscalar microprocessor correctness statements 298--312 Skander Kort and Sofi\`ene Tahar and Paul Curzon Hierarchical formal verification using a hybrid tool . . . . . . . . . . . . . . 313--322 Roope Kaivola and Katherine Kohatsu Proof engineering in the large: formal verification of Pentium\reg4 floating-point divider . . . . . . . . . 323--334 Fady Copty and Amitai Irron and Osnat Weissberg and Nathan Kropp and Gila Kamhi Efficient debugging in a formal verification environment . . . . . . . . 335--348 Koen Claessen and Mary Sheeran and Satnam Singh Using Lava to design and verify recursive and periodic sorters . . . . . 349--358 Xiaohua Kong and Radu Negulescu and Larry Weidong Ying Refinement-based formal verification with heterogeneous timing . . . . . . . 359--370 César Muñoz and Víctor Carreño and Gilles Dowek and Ricky Butler Formal verification of conflict detection algorithms . . . . . . . . . . 371--380 Karim El Guemhioui A framework for distributing object-oriented designs . . . . . . . . 381--396
Dieter Hogrefe Main issues in protocol testing . . . . 397--400 Bengt Jonsson and Konstantinos Sagonas Preface by the section editors . . . . . 401--404 Lars-Åke Fredlund and Dilian Gurov and Thomas Noll and Mads Dam and Thomas Arts and Gennady Chugunov A verification tool for ERLANG . . . . . 405--420 Erik Johansson and Mikael Pettersson and Konstantinos Sagonas and Thomas Lindgren The development of the HiPE system: design and experience report . . . . . . 421--436 Jakob Engblom and Andreas Ermedahl and Mikael Sjödin and Jan Gustafsson and Hans Hansson Worst-case execution-time analysis for embedded real-time systems . . . . . . . 437--455 John Håkansson and Bengt Jonsson and Ola Lundqvist Generating online test oracles from temporal logic specifications . . . . . 456--471 Mourad Debbabi and Nancy Durgin and Mohamed Mejri and John C. Mitchell Security by typing . . . . . . . . . . . 472--495 Shoham Ben-David and Orna Grumberg and Tamir Heyman and Assaf Schuster Scalable distributed on-the-fly symbolic model checking . . . . . . . . . . . . . 496--504 Yifei Dong and Xiaoqun Du and Gerard J. Holzmann and Scott A. Smolka Fighting livelock in the GNU i-protocol: a case study in explicit-state model checking . . . . . . . . . . . . . . . . 505--528
Tiziana Margaria and Wang Yi Introductory paper: scalability aspects of validation . . . . . . . . . . . . . 1--3 Poul F. Williams and Henrik R. Andersen and Henrik Hulgaard Satisfiability checking using Boolean Expression Diagrams . . . . . . . . . . 4--14 Tuba Yavuz-Kahveci and Tevfik Bultan A symbolic manipulator for automated verification of reactive systems with heterogeneous data types . . . . . . . . 15--33 Corina S. P\uas\uareanu and Matthew B. Dwyer and Willem Visser Finding feasible abstract counter-examples . . . . . . . . . . . . 34--48 Thomas Ball and Andreas Podelski and Sriram K. Rajamani Boolean and Cartesian abstraction for model checking C programs . . . . . . . 49--58 Brian Nielsen and Arne Skou Automated test generation from timed automata . . . . . . . . . . . . . . . . 59--77 Elsa L. Gunter and Anca Muscholl and Doron Peled Compositional message sequence charts 78--89 P. Chevalley and P. Thévenod-Fosse A mutation analysis tool for Java programs . . . . . . . . . . . . . . . . 90--103
Jaco van de Pol Introductory paper . . . . . . . . . . . 105--106 Tiziana Margaria and Bernhard Steffen Lightweight coarse-grained coordination: a scalable system-level approach . . . . 107--123 David Lugato and Céline Bigot and Yannick Valot and Jean-Pierre Gallois and Sébastien Gérard and François Terrier Validation and automatic test generation on UML models: the AGATHA approach . . . 124--139 A. Pretschner and O. Slotosch and E. Aiglstorfer and S. Kriebel Model-based testing for real: The inhouse card case study . . . . . . . . 140--157 Gordon Pace and Nicolas Halbwachs and Pascal Raymond Counter-example generation in symbolic abstract model-checking . . . . . . . . 158--164 María del Mar Gallardo and Jesús Martínez and Pedro Merino and Ernesto Pimentel aSPIN: a tool for abstract model checking . . . . . . . . . . . . . . . . 165--184 Viktor Schuppan and Armin Biere Efficient reduction of finite state model checking to reachability analysis 185--204 Thomas Arts and Clara Benac Earle and John Derrick Development of a verified Erlang program for resource locking . . . . . . . . . . 205--220 Conrado Daws and Marta Kwiatkowska and Gethin Norman Automatic verification of the IEEE 1394 root contention protocol with KRONOS and PRISM . . . . . . . . . . . . . . . . . 221--236 Sylvie Boldo and Marc Daumas Properties of two's complement floating point notations . . . . . . . . . . . . 237--246 Stefan Edelkamp and Stefan Leue and Alberto Lluch-Lafuente Directed explicit-state model checking in the validation of communication protocols . . . . . . . . . . . . . . . 247--267 Giorgio Delzanno and Jean-François Raskin and Laurent Van Begin Covering sharing trees: a compact data structure for parameterized verification 268--297
S. Purushothaman Iyer and David Hislop and Paul L. Jones and Jaime Lee and Frederick Pearce and Stephen Van Albert Introductory paper . . . . . . . . . . . 299--300 John C. Martin Formal methods software engineering for the CARA system . . . . . . . . . . . . 301--307 Rajeev Alur and David Arney and Elsa L. Gunter and Insup Lee and Jaime Lee and Wonhong Nam and Frederick Pearce and Steve Van Albert and Jiaxiang Zhou Formal specifications and analysis of the computer-assisted resuscitation algorithm (CARA) Infusion Pump Control System . . . . . . . . . . . . . . . . . 308--319 Raoul Praful Jetley and Cohan Carlos and S. Purushothaman Iyer A case study on applying formal methods to medical devices: computer-aided resuscitation algorithm . . . . . . . . 320--330 Eugene W. Stark Formally specifying CARA in Java . . . . 331--350 Arnab Ray and Rance Cleaveland Unit verification: the CARA experience 351--369 Luqi and Z. Guan and V. Berzins and L. Zhang and D. Floodeen and V. Coskun and J. Puett and M. Brown Requirements-document-based prototyping of CARA software . . . . . . . . . . . . 370--390
Lenore Zuck and Paul Attie and Agostino Cortesi Preface by the section editors . . . . . 1--3 Hardi Hungar and Bernhard Steffen Behavior-based model construction . . . 4--14 Xavier Rival Certification of compiled assembly code by invariant translation . . . . . . . . 15--37 Ping Yang and C. R. Ramakrishnan and Scott A. Smolka A logical encoding of the $\pi$-calculus: model checking mobile processes using tabled resolution . . . 38--66 Toh Ne Win and Michael D. Ernst and Stephen J. Garland and Dilsun Kimathrlimath and Nancy A. Lynch Using simulated execution in verifying distributed algorithms . . . . . . . . . 67--76 Farn Wang Efficient verification of timed automata with BDD-like data structures . . . . . 77--97
Joost-Pieter Katoen and Perdita Stevens Guest editors' introduction: Advancements and extensions of verification techniques . . . . . . . . 99--101 HoonSang Jin and Kavita Ravi and Fabio Somenzi Fate and free will in error traces . . . 102--116 Patrice Godefroid and Sarfraz Khurshid Exploring very large state spaces using genetic algorithms . . . . . . . . . . . 117--127 Marta Kwiatkowska and Gethin Norman and David Parker Probabilistic symbolic model checking with PRISM: a hybrid approach . . . . . 128--142 Fabrice Bouquet and Bruno Legeard and Fabien Peureux CLPS-B --- a constraint solver to animate a B specification . . . . . . . 143--157 Klaus Havelund and Grigore Ro\csu Efficient monitoring of safety properties . . . . . . . . . . . . . . . 158--173 Sérgio Campos and Orna Grumberg and Karen Yorav and Copty Fady Test sequence generation and model checking using dynamic transition relations . . . . . . . . . . . . . . . 174--182
Heiko Dörr and Andy Schürr Introduction . . . . . . . . . . . . . . 183--185 G. Schopfer and A. Yang and L. von Wedel and W. Marquardt CHEOPS: a tool-integration platform for chemical process modelling and simulation . . . . . . . . . . . . . . . 186--202 Sven Burmester and Holger Giese and Jörg Niere and Matthias Tichy and Jörg P. Wadsack and Robert Wagner and Lothar Wendehals and Albert Zündorf Tool integration at the meta-model level: the Fujaba approach . . . . . . . 203--218 Klaus Marius Hansen Thoth: a publish/subscribe architecture for peer-to-peer tool integration . . . 219--230 Flavio Corradini and Leonardo Mariani and Emanuela Merelli An agent-based approach to tool integration . . . . . . . . . . . . . . 231--244 Jean-Louis Colaço and Marc Pouzet Type-based initialization analysis of a synchronous dataflow language . . . . . 245--255
Matthew Dwyer and Stefan Leue Special section on the algorithmics of software model checking: Introductory paper . . . . . . . . . . . . . . . . . 257--259 Alex Groce and Willem Visser Heuristics for model checking Java programs . . . . . . . . . . . . . . . . 260--276 Stefan Edelkamp and Stefan Leue and Alberto Lluch-Lafuente Partial-order reduction and trail improvement in directed model checking 277--301 Radu Iosif Symmetry reductions for model checking of concurrent dynamic software . . . . . 302--319 Giuseppe Della Penna and Benedetto Intrigila and Igor Melatti and Enrico Tronci and Marisa Venturini Zilli Exploiting transition locality in automatic verification of finite-state concurrent systems . . . . . . . . . . . 320--341
Lubo\vs Brim and Orna Grumberg Special section on parallel and distributed model checking: Introductory paper . . . . . . . . . . . . . . . . . 1--3 Víctor Braberman and Alfredo Olivero and Fernando Schapachnik Issues in distributed timed model checking: Building Zeus . . . . . . . . 4--18 Gerd Behrmann Distributed reachability analysis in timed automata . . . . . . . . . . . . . 19--30 Michael D. Jones and Jacob Sorber Parallel search for LTL violations . . . 31--42 Alexander Bell and Boudewijn R. Haverkort Sequential and distributed model checking of Petri nets . . . . . . . . . 43--60 Lubo\vs Brim and Karen Yorav and Jitka \vZídková Assumption-based distribution of CTL model checking . . . . . . . . . . . . . 61--73 Stefan Blom and Simona Orzan A distributed algorithm for strong bisimulation reduction of state spaces 74--86
Armin Biere and Ofer Strichman Introductory paper: Highlights from the BMC'03 workshop and more . . . . . . . . 87--88 Toni Jussila and Keijo Heljanko and Ilkka Niemelä BMC via on-the-fly determinization . . . 89--101 Gianpiero Cabodi and Alex Kondratyev and Luciano Lavagno and Sergio Nocco and Stefano Quer and Yosinori Watanabe A BMC-based formulation for the scheduling problem of hardware systems 102--117 Rajeev Alur and P. Madhusudan and Wonhong Nam Symbolic computational techniques for solving games . . . . . . . . . . . . . 118--128 Gianpiero Cabodi and Sergio Nocco and Stefano Quer Are BDDs still alive within sequential verification? . . . . . . . . . . . . . 129--142 Bing Li and Chao Wang and Fabio Somenzi Abstraction refinement in symbolic model checking using satisfiability as the only decision procedure . . . . . . . . 143--155 Mukul R. Prasad and Armin Biere and Aarti Gupta A survey of recent advances in SAT-based formal verification . . . . . . . . . . 156--173 Edmund Clarke and Daniel Kroening and Joël Ouaknine and Ofer Strichman Computational challenges in bounded model checking . . . . . . . . . . . . . 174--183 Martin Leucker and Thomas Noll and Perdita Stevens and Michael Weber Functional programming languages for verification tools: a comparison of Standard ML and Haskell . . . . . . . . 184--194
Thomas Arts and Jaco van de Pol Special section on formal methods for industrial critical systems: Introductory paper . . . . . . . . . . . 195--196 Richard Bubel and Reiner Hähnle Integration of informal and formal development of object-oriented safety-critical software . . . . . . . . 197--211 Lilian Burdy and Yoonsik Cheon and David R. Cok and Michael D. Ernst and Joseph R. Kiniry and Gary T. Leavens and K. Rustan M. Leino and Erik Poll An overview of JML tools and applications . . . . . . . . . . . . . . 212--232 Achim D. Brucker and Burkhart Wolff A verification approach to applied system security . . . . . . . . . . . . 233--247 Andrew Butterfield and Jim Woodcock prialt in Handel-C: an operational semantics . . . . . . . . . . . . . . . 248--267 Jerker Hammarberg and Simin Nadjm-Tehrani Formal verification of fault tolerance in safety-critical reconfigurable modules . . . . . . . . . . . . . . . . 268--279 Stefan Blom and Simona Orzan Distributed state space minimization . . 280--291
Tiziana Margaria Introductory paper . . . . . . . . . . . 293--296 Claude Jard and Thierry Jéron TGV: theory, principles and algorithms 297--315 César Viho Test distribution: a solution for complex network system testing . . . . . 316--325 Andrea Baldini and Alfredo Benso and Paolo Prinetto System-level functional testing from UML specifications in end-of-production industrial environments . . . . . . . . 326--340 Annette Bunker and Ganesh Gopalakrishnan and Konrad Slind Live sequence charts applied to hardware requirements specification and verification . . . . . . . . . . . . . . 341--350 Ina Schieferdecker and George Din and Dimitrios Apostolidis Distributed functional and load tests for Web services . . . . . . . . . . . . 351--360 Kenneth J. Turner Test generation for radiotherapy accelerators . . . . . . . . . . . . . . 361--375 Bartholomäus Kellerer and Manfred Reitenspiess Practical quality assurance for standards-based, high-availability middleware . . . . . . . . . . . . . . . 376--387
Hubert Garavel and John Hatcliff Why you should definitely read this special section . . . . . . . . . . . . 1--3 Gianfranco Ciardo and Robert Marmorstein and Radu Siminiceanu The saturation algorithm for symbolic state-space exploration . . . . . . . . 4--25 Constantinos Bartzis and Tevfik Bultan Efficient BDDs for bounded arithmetic constraints . . . . . . . . . . . . . . 26--36 Radu Mateescu CAESAR\_SOLVE: a generic library for on-the-fly resolution of alternation-free Boolean equation systems . . . . . . . . . . . . . . . . 37--56 L. Bozga and Y. Lakhnech and M. Périn Pattern-based abstraction for verifying secrecy in protocols . . . . . . . . . . 57--76 Jan Friso Groote and Frank van Ham Interactive visualization of large state spaces . . . . . . . . . . . . . . . . . 77--91
Susanne Graf and Òystein Haugen and Ileana Ober and Bran Selic Preface of ``Specification and Validation of Real Time and Embedded systems in UML'' . . . . . . . . . . . . 93--96 Jozef Hooman and Mark B. van der Zwaag A semantics of communicating reactive objects with timing . . . . . . . . . . 97--112 Susanne Graf and Ileana Ober and Iulian Ober A real-time profile for UML . . . . . . 113--127 Iulian Ober and Susanne Graf and Ileana Ober Validating timed UML models by simulation and verification . . . . . . 128--145 Robert de Simone and Charles André Towards a ``Synchronous Reactive'' UML profile? . . . . . . . . . . . . . . . . 146--155 Juliana Küster-Filipe and Stuart Anderson On a time enriched OCL liveness template 156--166 Kirsten Berkenkötter and Stefan Bisanz and Ulrich Hannemann and Jan Peleska The HybridUML profile for UML 2.0 . . . 167--176
Kurt Jensen and Andreas Podelski Tools and algorithms for the construction and analysis of systems . . 177--179 Antti Valmari What the small Rubik's cube taught me about data structures, information theory, and randomisation . . . . . . . 180--194 Karsten Schmidt Automated generation of a progress measure for the sweep-line method . . . 195--203 Gerd Behrmann and Patricia Bouyer and Kim G. Larsen and Radek Pelánek Lower and upper bounds in zone-based abstractions of timed automata . . . . . 204--215 Håkan L. S. Younes and Marta Kwiatkowska and Gethin Norman and David Parker Numerical vs. statistical probabilistic model checking . . . . . . . . . . . . . 216--228 Alex Groce and Sagar Chaki and Daniel Kroening and Ofer Strichman Error explanation with distance metrics 229--247 Koushik Sen and Grigore Rosu and Gul Agha Online efficient predictive safety analysis of multithreaded programs . . . 248--260 Yi Fang and Nir Piterman and Amir Pnueli and Lenore Zuck Liveness with invisible ranking . . . . 261--279 Robby and Edwin Rodríguez and Matthew B. Dwyer and John Hatcliff Checking JML specifications using an extensible software model checking framework . . . . . . . . . . . . . . . 280--299
John S. Fitzgerald and Stefania Gnesi and Dino Mandrioli The industrialization of formal methods 301--302 Steven P. Miller and Alan C. Tribble and Michael W. Whalen and Mats P. E. Heimdahl Proving the shalls . . . . . . . . . . . 303--319 C. J. Fidge Formal change impact analyses for emulated control software . . . . . . . 321--335 Alan Wassyng and Mark Lawford Software tools for safety-critical software development . . . . . . . . . . 337--354 Enrico Tronci Introductory Paper . . . . . . . . . . . 355--358 J. Strother Moore Inductive assertions and operational semantics . . . . . . . . . . . . . . . 359--371 Hana Chockler and Orna Kupferman and Moshe Vardi Coverage metrics for formal verification 373--386 Malay K. Ganai and Aarti Gupta and Zijiang Yang and Pranav Ashar Efficient distributed SAT and SAT-based distributed Bounded Model Checking . . . 387--396 Giuseppe Della Penna and Benedetto Intrigila and Igor Melatti and Enrico Tronci and Marisa Venturini Zilli Finite horizon analysis of Markov Chains with the Mur$\phi$ verifier . . . . . . 397--409 Sven Beyer and Christian Jacobi and Daniel Kröning and Dirk Leinenbach and Wolfgang J. Paul Putting it all together --- Formal verification of the VAMP . . . . . . . . 411--430
Tiziana Margaria and Bernhard Steffen Special Section on ``Leveraging Formal Methods'' . . . . . . . . . . . . . . . 467--469 François Carcenac and Frederic Boniol A formal framework for verifying distributed embedded systems based on abstraction methods . . . . . . . . . . 471--484 Jesper Andersen and Ebbe Elsborg and Fritz Henglein and Jakob Grue Simonsen and Christian Stefansen Compositional specification of commercial contracts . . . . . . . . . . 485--516 Erwan Jahier and Pascal Raymond and Philippe Baufreton Case studies with Lurette V2 . . . . . . 517--530 Jens Bæk Jòrgensen and Sòren Christensen and Antti-Pekka Tuovinen and Jianli Xu Tool Support for Estimating the Memory Usage of Mobile Phone Software . . . . . 531--545 Yamine Ait-Ameur and Mickael Baron Formal and experimental validation approaches in HCI systems design based on a shared event B model . . . . . . . 547--563 M. Alpuente and D. Ballis and M. Falaschi Rule-based verification of Web sites . . 565--585 Christopher A. Rouff and Michael G. Hinchey and Walter F. Truszkowski and James L. Rash Experiences applying formal approaches in the development of swarm-based space exploration systems . . . . . . . . . . 587--603 Peter Buchholz and Joost-Pieter Katoen and Marcel Verhoef Guest Editors' introduction: quantitative analysis of real-time embedded systems . . . . . . . . . . . . 605--606 Joern Ploennigs and Mario Neugebauer and Klaus Kabitzsch Automated model generation for performance engineering of building automation networks . . . . . . . . . . 607--620
Deepak D'Souza and Pavithra Prabhakar On the expressiveness of MTL in the pointwise and continuous semantics . . . 1--4 Marco Bozzano and Adolfo Villafiorita The FSAP/NuSMV-SA Safety Analysis Platform . . . . . . . . . . . . . . . . 5--24 Michael Huth Some current topics in model checking 25--36 Aleksandar Dimovski and Ranko Lazi\'c Compositional software verification based on game semantics and process algebra . . . . . . . . . . . . . . . . 37--51 Dimitar P. Guelev and Mark D. Ryan and Pierre Yves Schobbens Model-checking the preservation of temporal properties upon feature integration . . . . . . . . . . . . . . 53--62 Radu I. Siminiceanu and Gianfranco Ciardo Formal verification of the NASA runway safety monitor . . . . . . . . . . . . . 63--76 Cécile Braunstein and Emmanuelle Encrenaz CTL-property Transformations along an Incremental Design Process . . . . . . . 77--88 Shobha Vasudevan and E. Allen Emerson and Jacob A. Abraham Improved verification of hardware designs through antecedent conditioned slicing . . . . . . . . . . . . . . . . 89--101
Dragan Ga\vsevi\'c and Dragan Djuri\'c and Vladan Deved\vzi\'c MDA-based Automatic OWL Ontology Development . . . . . . . . . . . . . . 103--117 Orna Grumberg and Shmuel Katz VeriTech: a framework for translating among model description notations . . . 119--132 Mauro Pezz\`e Introduction to the special section on FASE 2003 . . . . . . . . . . . . . . . 133--134 Wim Vanderperren and Davy Suvée and Bruno De Fraine and Viviane Jonckers Aspect-oriented Component Composition in PacoSuite Through Invasive Composition Adapters . . . . . . . . . . . . . . . . 135--154 Ioana Sora and Pierre Verbaeten and Yolande Berbers CCDL: the Composable Components Description Language . . . . . . . . . . 155--168 Claus Pahl An ontology for software component matching . . . . . . . . . . . . . . . . 169--178 Vieri del Bianco and Luigi Lavazza and Marco Mauri and Giuseppe Occorso Towards UML-based formal specifications of component-based real-time software 179--192 Reiko Heckel and Marc Lohmann Model-driven development of reactive information systems: from graph transformation rules to JML contracts 193--207
Kurt Jensen Special section on coloured Petri nets 209--212 Kurt Jensen and Lars Michael Kristensen and Lisa Wells Coloured Petri Nets and CPN Tools for modelling and validation of concurrent systems . . . . . . . . . . . . . . . . 213--254 Brice Mitchell and Lars Michael Kristensen and Lin Zhang Formal specification and state space analysis of an operational planning process . . . . . . . . . . . . . . . . 255--267 Jonathan Billington and Bing Han Modelling and analysing the functional behaviour of TCP's connection management procedures . . . . . . . . . . . . . . . 269--304 Lin Liu and Jonathan Billington Verification of the Capability Exchange Signalling protocol . . . . . . . . . . 305--326 Maja Pesic and Wil M. P. van der Aalst Modelling work distribution mechanisms using Colored Petri Nets . . . . . . . . 327--352 Ricardo J. Machado and Kristian Bisgaard Lassen and Sérgio Oliveira and Marco Couto and Patrícia Pinto Requirements Validation: Execution of UML Models with CPN Tools . . . . . . . 353--369 Guy Edward Gallasch and Jonathan Billington and Somsak Vanit-Anunchai and Lars Michael Kristensen Checking safety properties on-the-fly with the sweep-line method . . . . . . . 371--391 C. Lakos and L. Petrucci Modular state space exploration for timed Petri nets . . . . . . . . . . . . 393--411 Roberto Bagnara and Patricia M. Hill and Enea Zaffanella Widening operators for powerset domains 413--414
Michel Wermelinger and Tiziana Margaria and Maura Cerioli Introduction to the special section on fundamental approaches to software engineering . . . . . . . . . . . . . . 415--416 Georg Jung and John Hatcliff A correlation framework for the CORBA component model . . . . . . . . . . . . 417--427 Marsha Chechik and Arie Gurfinkel A framework for counterexample generation and exploration . . . . . . . 429--445 Grégoire Hamon and John Rushby An operational semantics for Stateflow 447--456 Ruth Breu and Gerhard Popp and Muhammad Alam Model based development of access policies . . . . . . . . . . . . . . . . 457--470 Kim G. Larsen and Ulrik Nyman and Andrzej Wasowski Modeling software product lines using color-blind transition systems . . . . . 471--487 Venkatesh Prasad Ranganath and John Hatcliff Slicing concurrent Java programs using Indus and Kaveri . . . . . . . . . . . . 489--504 Dirk Beyer and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar The software model checker \sc Blast . . 505--525 Jan Jürjens and Pasha Shabalin Tools for secure systems development with UML . . . . . . . . . . . . . . . . 527--544
Kurt Jensen Special section on Coloured Petri Nets 1--3 Lars M. Kristensen and Peter Mechlenborg and Lin Zhang and Brice Mitchell and Guy E. Gallasch Model-based development of a course of action scheduling tool . . . . . . . . . 5--14 Jens Bæk Jòrgensen and Kristian Bisgaard Lassen and Wil M. P. van der Aalst From task descriptions via colored Petri nets towards an implementation of a new electronic patient record workflow system . . . . . . . . . . . . . . . . . 15--28 Somsak Vanit-Anunchai and Jonathan Billington and Guy Edward Gallasch Analysis of the Datagram Congestion Control Protocol's connection management procedures using the sweep-line method 29--56 A. Rozinat and R. S. Mans and M. Song and W. M. P. van der Aalst Discovering colored Petri nets from event logs . . . . . . . . . . . . . . . 57--74 Guy Edward Gallasch and Nimrod Lilith and Jonathan Billington and Lin Zhang and Axel Bender and Benjamin Francis Modelling defence logistics networks . . 75--93 F. Gottschalk and W. M. P. van der Aalst and M. H. Jansen-Vullers and H. M. W. Verbeek Protos2CPN: using colored Petri nets for configuring and testing business processes . . . . . . . . . . . . . . . 95--110
Holger Hermanns and Jens Palsberg Improving the effectiveness of system verification . . . . . . . . . . . . . . 111--112 Dina Thomas and Supratik Chakraborty and Paritosh Pandya Efficient guided symbolic reachability using reachability expressions . . . . . 113--129 Alex Groce and Rajeev Joshi Exploiting traces in static program analysis: better model checking through printfs . . . . . . . . . . . . . . . . 131--144 Atul Gupta and Pankaj Jalote An approach for experimentally evaluating effectiveness and efficiency of coverage criteria for software testing . . . . . . . . . . . . . . . . 145--160 Javier Esparza and Pradeep Kanade and Stefan Schwoon A negative result on depth-first net unfoldings . . . . . . . . . . . . . . . 161--166 Rachid Hadjidj and Hanifa Boucheneb Improving state class constructions for CTL* model checking of time Petri nets 167--184 Michael Leuschel and Michael Butler ProB: an automated analysis toolset for the B method . . . . . . . . . . . . . . 185--203
Wilhelm Schäfer and Matthias Tichy Introduction to the special section on self-optimizing mechatronic systems . . 205--206 Sven Burmester and Holger Giese and Eckehard Münch and Oliver Oberschelp and Florian Klein and Peter Scheideler Tool support for the design of self-optimizing mechatronic multi-agent systems . . . . . . . . . . . . . . . . 207--222 Katrin Witting and Bernd Schulz and Michael Dellnitz and Joachim Böcker and Norbert Fröhleke A new approach for online multiobjective optimization of mechatronic systems . . 223--231 Benno Stein Coping with large design spaces: design problem solving in fluidic engineering 233--245 Mircea Trofin and John Murphy Static verification of component composition in contextual composition frameworks . . . . . . . . . . . . . . . 247--261 Goran Frehse PHAVer: algorithmic verification of hybrid systems past HyTech . . . . . . . 263--279
Ina Schieferdecker and Jens Grabowski Introduction to the special section on advances in test automation: the evolution of TTCN-3 . . . . . . . . . . 281--283 Martin Botteck and Thomas Deiß Introduction of TTCN-3 into the product development process: considerations from an electronic devices developer point of view . . . . . . . . . . . . . . . . . . 285--289 Andrej Pietschker Automating test automation . . . . . . . 291--295 Markus Warken From testing to anti-product development 297--307 Helmut Neukirchen and Benjamin Zeiss and Jens Grabowski An approach to quality engineering of TTCN-3 test specifications . . . . . . . 309--326 Stephan Schulz Test suite development with TTCN-3 libraries . . . . . . . . . . . . . . . 327--336 Ariel Sabiguero and Anthony Baire and César Viho Automatic CoDec generation to reduce test engineering cost . . . . . . . . . 337--346 Thomas Deiß Refactoring and converting a TTCN-2 test suite . . . . . . . . . . . . . . . . . 347--352 Michael Gläser and Sebastian Müller and Axel Rennoch and Peter Schmitting Standardized TTCN-3 specifications for SIP-ISUP/ISDN interworking testing . . . 353--358 George Din An IMS Performance Benchmark Implementation based on the TTCN-3 Language . . . . . . . . . . . . . . . . 359--370 Bernard Stepien and Liam Peyton and Pulei Xiong Framework testing of Web applications using TTCN-3 . . . . . . . . . . . . . . 371--381 Ina Schieferdecker and Juergen Grossmann Testing hybrid control systems with TTCN-3: an overview on continuous TTCN-3 383--400
Sébastien Bardin and Alain Finkel and Jérôme Leroux and Laure Petrucci FAST: acceleration from theory to practice . . . . . . . . . . . . . . . . 401--424 Jörn Ossowski and Christel Baier A uniform framework for weighted decision diagrams and its implementation 425--441 Radek Pelánek Properties of state spaces and their applications . . . . . . . . . . . . . . 443--454 Ali Ebnenasir and Sandeep S. Kulkarni and Anish Arora FTSyn: a framework for automatic synthesis of fault-tolerance . . . . . . 455--471
Alessandro Marchetto Special section on testing and security of Web systems . . . . . . . . . . . . . 473--476 Alessandro Marchetto and Filippo Ricca and Paolo Tonella A case study-based comparison of Web testing techniques applied to AJAX Web applications . . . . . . . . . . . . . . 477--492 Antonio Carzaniga and Alessandra Gorla and Mauro Pezz\`e Healing Web applications through automatic workarounds . . . . . . . . . 493--502 Graham Hughes and Tevfik Bultan Automated verification of access control policies using a SAT solver . . . . . . 503--520 Sebastian Kinder and Rolf Drechsler Modeling and proving functional completeness in formal verification of counting heads . . . . . . . . . . . . . 521--534
Antti Valmari Software model checking is a rich research field . . . . . . . . . . . . . 1--11 I. Melatti and R. Palmer and G. Sawaya and Y. Yang and R. M. Kirby and others Parallel and distributed model checking in Eddy . . . . . . . . . . . . . . . . 13--25 Klaus Dräger and Bernd Finkbeiner and Andreas Podelski Directed model checking with distance-preserving abstractions . . . . 27--37 Dragan Bosnacki and Stefan Leue and Alberto Lluch Lafuente Partial-order reduction for general state exploring algorithms . . . . . . . 39--51 Saswat Anand and Corina S. Pasareanu and Willem Visser Symbolic execution with abstraction . . 53--67 Alessandro Armando and Jacopo Mantovani and Lorenzo Platania Bounded model checking of software using SMT solvers instead of SAT solvers . . . 69--83
Michael Huth and Orna Grumberg Special section on advances in reachability analysis and decision procedures: contributions to abstraction-based system verification 85--94 Randal E. Bryant and Daniel Kroening and Joël Ouaknine and Sanjit A. Seshia and Ofer Strichman and Bryan Brady An abstraction-based decision procedure for bit-vector arithmetic . . . . . . . 95--104 Shaunak Chatterjee and Shuvendu K. Lahiri and Shaz Qadeer and Zvonimir Rakamari\'c A low-level memory model and an accompanying reachability predicate . . 105--116 Andy Jinqing Yu and Gianfranco Ciardo and Gerald Lüttgen Decision-diagram-based techniques for bounded reachability checking of asynchronous systems . . . . . . . . . . 117--131 Lili Tan The worst-case execution time tool challenge 2006 . . . . . . . . . . . . . 133--152 Chryssis Georgiou and Nancy Lynch and Panayiotis Mavrommatis and Joshua A. Tauber Automated implementation of complex distributed algorithms specified in the IOA language . . . . . . . . . . . . . . 153--171
Mike Hinchey and Tiziana Margaria and Bernhard Steffen Guest Editor's introduction . . . . . . 173--174 Boutheina Chetali and Quang-Huy Nguyen An automated testing experiment for layered embedded C code . . . . . . . . 175--185 Bastian Schlich and Stefan Kowalewski Model checking C source code for embedded systems . . . . . . . . . . . . 187--202 Eric Van Wyk and Mats Per Erik Heimdahl Flexibility in modeling languages and tools: a call to arms . . . . . . . . . 203--215 Dominique Cansell and Dominique Méry and Cyril Proch System-on-chip design by proof-based refinement . . . . . . . . . . . . . . . 217--238 Yamine Ait-Ameur and Mickael Baron and Nadjet Kamel and Jean-Marc Mota Encoding a process algebra using the Event B method Application to the validation of human-computer interactions . . . . . . . . . . . . . . 239--253 David Déharbe and Silvio Ranise Satisfiability solving for software verification . . . . . . . . . . . . . . 255--260 Alexandra Desmoulin and César Viho Formalizing interoperability for test case generation purpose . . . . . . . . 261--267
Karen Yorav Haifa verification conference 2007 . . . 269--272 Benny Pasternak and Shmuel Tyszberowicz and Amiram Yehudai GenUTest: a unit test and mock aspect generation tool . . . . . . . . . . . . 273--290 Shai Fine and Laurent Fournier and Avi Ziv Using Bayesian networks and virtual coverage to hit hard-to-reach events . . 291--305 Harald Raffelt and Maik Merten and Bernhard Steffen and Tiziana Margaria Dynamic testing via automata learning 307--324 Domagoj Babi\'c and Alan J. Hu Approximating the safely reusable set of learned facts . . . . . . . . . . . . . 325--338 Corina S. Pasareanu and Willem Visser A survey of new trends in symbolic execution for software testing and analysis . . . . . . . . . . . . . . . . 339--353
Tiziana Margaria and Mieke Massink Preface . . . . . . . . . . . . . . . . 355--357 Pedro de la Cámara and María del Mar Gallardo and Pedro Merino and David Sanán Checking the reliability of socket based communication software . . . . . . . . . 359--374 Anton J. Wijs and Jaco C. van de Pol and Elena M. Bortnik Solving scheduling problems by untimed model checking: The clinical chemical analyser case study . . . . . . . . . . 375--392 Harald Raffelt and Bernhard Steffen and Therese Berg and Tiziana Margaria LearnLib: a framework for extrapolating behavioral models . . . . . . . . . . . 393--407 Jan Mikác and Paul Caspi Flush: an example of development by refinements in SCADE/Lustre . . . . . . 409--418
Filippo Ricca and Liu Chao Special section on Web Systems Evolution 419--425 Alessandro Marchetto and Filippo Ricca From objects to services: toward a stepwise migration approach for Java applications . . . . . . . . . . . . . . 427--440 Harry M. Sneed A pilot project for migrating COBOL code to Web services . . . . . . . . . . . . 441--451 Keisuke Nakano and Zhenjiang Hu and Masato Takeichi Consistent Web site updating based on bidirectional transformation . . . . . . 453--468 Giuseppe Scanniello and Damiano Distante and Michele Risi An approach and an Eclipse-based environment for enhancing the navigation structure of Web sites . . . . . . . . . 469--484 Mario Luca Bernardi and Giuseppe Antonio Di Lucca and Damiano Distante The RE-UWA approach to recover user centered conceptual models from Web applications . . . . . . . . . . . . . . 485--501 Brian Chan and King Chun Foo and Lionel Marks and Ying Zou An approach for estimating the time needed to perform code changes in business applications . . . . . . . . . 503--515
Yamine Ait Ameur and Frédéric Boniol and Virginie Wiels Toward a wider use of formal methods for aerospace systems design and verification . . . . . . . . . . . . . . 1--7 Daniel Plagge and Michael Leuschel Seven at one stroke: LTL model checking for high-level specifications in B, Z, CSP, and more . . . . . . . . . . . . . 9--21 Andreas Bauer and Martin Leucker and Christian Schallhart and Michael Tautschnig Don't care in SMT: building flexible yet efficient abstraction/refinement solvers 23--37 Joris Rehm Proved development of the real-time properties of the IEEE 1394 Root Contention Protocol with the event-B method . . . . . . . . . . . . . . . . . 39--51 Shlomi Dolev and Ori Gersten A framework for robust active super tier systems . . . . . . . . . . . . . . . . 53--67 Richard H. Carver and Yu Lei A class library for implementing, testing, and debugging concurrent programs . . . . . . . . . . . . . . . . 69--88
Dragan Bosnacki and Stefan Edelkamp Model checking software: on some new waves and some evergreens . . . . . . . 89--95 Michael Weber An embeddable virtual machine for state space generation . . . . . . . . . . . . 97--111 Yu Yang and Xiaofang Chen and Ganesh Gopalakrishnan and Robert M. Kirby Distributed dynamic partial order reduction . . . . . . . . . . . . . . . 113--122 Kristin Y. Rozier and Moshe Y. Vardi LTL satisfiability checking . . . . . . 123--137 J. Barnat and L. Brim and P. Rockai Scalable shared memory LTL model checking . . . . . . . . . . . . . . . . 139--153 Sami Evangelista and Christophe Pajault Solving the ignoring problem for partial order reduction . . . . . . . . . . . . 155--170
Arend Rensink and Pieter Van Gorp Graph transformation tool contest 2008 171--181 Javier Pérez and Yania Crespo and Berthold Hoffmann and Tom Mens A case study to evaluate the suitability of graph transformation tools for program refactoring . . . . . . . . . . 183--199 Olaf Muliawan and Dirk Janssens Model refactoring using MoTMoT . . . . . 201--209 Ákos Horváth and Gábor Bergmann and István Ráth and Dániel Varró Experimental assessment of combining pattern matching strategies with VIATRA2 211--230 Tamás Mészáros and Gergely Mezei and Tihamér Levendovszky and Márk Asztalos Manual and automated performance optimization of model transformation systems . . . . . . . . . . . . . . . . 231--243 Enrico Biermann and Claudia Ermel and Leen Lambers and Ulrike Prange and Olga Runge and others Introduction to AGG and EMF Tiger by modeling a Conference Scheduling System 245--261 Edgar Jakumeit and Sebastian Buchwald and Moritz Kroll GrGen.NET: The expressive, convenient and fast graph rewrite system . . . . . 263--271 Naouel Moha and Sagar Sen and Cyril Faucher and Olivier Barais and Jean-Marc Jézéquel Evaluation of Kermeta for solving graph-based problems . . . . . . . . . . 273--285 Leif Geiger and Albert Zündorf Fujaba case studies for GraBaTs 2008: lessons learned . . . . . . . . . . . . 287--304
Angelika Mader and Henrik Bohnenkamp and Yaroslav S. Usenko and David N. Jansen and Johann Hurink and Holger Hermanns Synthesis and stochastic assessment of cost-optimal schedules . . . . . . . . . 305--318 Jocelyn Simmonds and Jessica Davies and Arie Gurfinkel and Marsha Chechik Exploiting resolution proofs to speed up LTL vacuity detection for BMC . . . . . 319--335 Vincent Beaudenon and Emmanuelle Encrenaz and Sami Taktak Data decision diagrams for Promela systems analysis . . . . . . . . . . . . 337--352 Holger Krahn and Bernhard Rumpe and Steven Völkel MontiCore: a framework for compositional development of domain specific languages 353--372 Adam Bakewell and Aleksandar Dimovski and Dan R. Ghica and Ranko Lazi\'c Data-abstraction refinement: a game semantic approach . . . . . . . . . . . 373--389 Giacomo Bucci and Laura Carnevali and Lorenzo Ridi and Enrico Vicario Oris: a tool for modeling, verification and evaluation of real-time systems . . 391--403
Daniel Kroening and Tiziana Margaria Verified software: theories, tools and experiments . . . . . . . . . . . . . . 405--408 Arie Gurfinkel and Sagar Chaki Combining predicate and numeric abstraction for software model checking 409--427 Patrice Chalin and Robby and Perry R. James and Jooyong Lee and George Karabotsos Towards an industrial grade IVE for Java and next generation research platform for JML . . . . . . . . . . . . . . . . 429--446 Jean-Raymond Abrial and Michael Butler and Stefan Hallerstede and Thai Son Hoang and Farhad Mehta and others Rodin: an open toolset for modelling and reasoning in Event-B . . . . . . . . . . 447--466 David R. Cok Improved usability and performance of SMT solvers for debugging specifications 467--481
Corina S. Pasareanu New results in software model checking and analysis . . . . . . . . . . . . . . 1--2 Ernst Moritz Hahn and Holger Hermanns and Lijun Zhang Probabilistic reachability for parametric Markov models . . . . . . . . 3--19 Dragan Bosnacki and Stefan Edelkamp and Damian Sulewski and Anton Wijs Parallel probabilistic model checking on general purpose graphics processors . . 21--35 Nicholas Kidd and Peter Lammich and Tayssir Touili and Thomas Reps A decision procedure for detecting atomicity violations for communicating processes with locks . . . . . . . . . . 37--60 Junghee Lim and Akash Lal and Thomas Reps Symbolic analysis via semantic reinterpretation . . . . . . . . . . . . 61--87 Sebastian Schmerl and Michael Vogel and Hartmut König Using model checking to identify errors in intrusion detection signatures . . . 89--106
Ying Zou and Ji Wu and Kenny Wong Guest editors' introduction to the special section from the International Symposium on Web Systems Evolution . . . 107--109 Kinga Dobolyi and Elizabeth Soechting and Westley Weimer Automating regression testing using Web-based application similarities . . . 111--129 Alessandro Marchetto and Roberto Tiella and Paolo Tonella and Nadia Alshahwan and Mark Harman Crawlability metrics for automated Web testing . . . . . . . . . . . . . . . . 131--149 Marco Torchiano and Filippo Ricca and Alessandro Marchetto Are Web applications more defect-prone than desktop applications? . . . . . . . 151--166 Adina Mosincat and Walter Binder Automated maintenance of service compositions with SLA violation detection and dynamic binding . . . . . 167--179 Marco D'Ambros and Michele Lanza and Mircea Lungu and Romain Robbes On porting software visualization tools to the web . . . . . . . . . . . . . . . 181--200
Hana Chockler and Alan J. Hu Preface . . . . . . . . . . . . . . . . 201--205 Yoram Adler and Dale Blue and Thomas Conti and Richard Prewitt and Shmuel Ur Evaluating workloads using comparative functional coverage . . . . . . . . . . 207--221 Cyrille Artho Iterative delta debugging . . . . . . . 223--246 Dorit Baras and Shai Fine and Laurent Fournier and Dan Geiger and Avi Ziv Automatic boosting of cross-product coverage using Bayesian networks . . . . 247--261 Omer Bar-Ilan and Oded Fuhrmann and Shlomo Hoory and Ohad Shacham and Ofer Strichman Reducing the size of resolution proofs in linear time . . . . . . . . . . . . . 263--272 K. Bauer and R. Gentilini and K. Schneider A uniform approach to three-valued semantics for $\mu$-calculus on abstractions of hybrid automata . . . . 273--287
Harald Fecher and Sharon Shoham Local abstraction-refinement for the $\mu$-calculus . . . . . . . . . . . . . 289--306 Lei Bu and Xuandong Li Path-oriented bounded reachability analysis of composed linear hybrid systems . . . . . . . . . . . . . . . . 307--317 Roberto Sebastiani and Stefano Tonetta and Moshe Y. Vardi Symbolic systems, explicit properties: on hybrid approaches for LTL symbolic model checking . . . . . . . . . . . . . 319--335 Liana Barachisio Lisboa and Vinicius Cardoso Garcia and Eduardo Santana de Almeida and Silvio Romero de Lemos Meira ToolDAy: a tool for domain analysis . . 337--353 Qiang Guo and John Derrick Formally based tool support for model checking Erlang applications . . . . . . 355--376 Olga Brukman and Shlomi Dolev Recovery oriented programming: runtime monitoring of safety and liveness . . . 377--395
Jean-Christophe Filliâtre Deductive software verification . . . . 397--403 Pascal Cuoq and Benjamin Monate and Anne Pacalet and Virgile Prevosto Functional dependencies of C functions via weakest pre-conditions . . . . . . . 405--417 Tjark Weber SMT solvers: new oracles for the HOL theorem prover . . . . . . . . . . . . . 419--429 Kalou Cabrera Castillos and Frédéric Dadeau and Jacques Julliand Scenario-based testing from UML/OCL behavioral models: Application to POSIX compliance . . . . . . . . . . . . . . . 431--448 Daisuke Ishii and Kazunori Ueda and Hiroshi Hosobe An interval-based SAT modulo ODE solver for model checking nonlinear hybrid systems . . . . . . . . . . . . . . . . 449--461 Leo Freitas and John McDermott Formal methods for security in the Xenon hypervisor . . . . . . . . . . . . . . . 463--489
Neil D. Jones and Markus Müller-Olm Preface to a special section on verification, model checking, and abstract interpretation . . . . . . . . 491--493 Nicholas Kidd and Thomas Reps and Julian Dolby and Mandana Vaziri Finding concurrency-related bugs using random isolation . . . . . . . . . . . . 495--518 Ankur Taly and Sumit Gulwani and Ashish Tiwari Synthesizing switching logic using constraint solving . . . . . . . . . . . 519--535 Kousha Etessami and Patrice Godefroid An abort-aware model of transactional programming . . . . . . . . . . . . . . 537--551 Michal Rutkowski and Ranko Lazi\'c and Marcin Jurdzi\'nski Average-price-per-reward games on hybrid automata with strong resets . . . . . . 553--569 Patrice Godefroid and Nir Piterman LTL generalized model checking revisited 571--584 Vincent Laviron and Francesco Logozzo SubPolyhedra: a family of numerical abstract domains for the (more) scalable inference of linear inequalities . . . . 585--601
Natasha Sharygina and Stefano Tonetta and Aliaksei Tsitovich An abstraction refinement approach combining precise and approximated techniques . . . . . . . . . . . . . . . 1--14 Amir Hossein Ghamarian and Maarten de Mol and Arend Rensink and Eduardo Zambon and Maria Zimakova Modelling and analysis using GROOVE . . 15--40 Shmuel Katz and David Faitelson The Common Aspect Proof Environment . . 41--52 Ananda Basu and Saddek Bensalem and Marius Bozga and Beno\^\it Delahaye and Axel Legay Statistical abstraction and model-checking of large heterogeneous systems . . . . . . . . . . . . . . . . 53--72 Alain Denise and Marie-Claude Gaudel and Sandrine-Dominique Gouraud and Richard Lassaigne and Johan Oudinet and others Coverage-biased random exploration of large models and application to testing 73--93 Georgia Penido Safe and Claudionor Coelho and Luiz Filipe M. Vieira and Celina Gomes Do Val and Jose Augusto Nacif and others Selection of formal verification heuristics for parallel execution . . . 95--108
Parosh Aziz Abdulla Regular model checking . . . . . . . . . 109--118 Axel Legay Extrapolating (omega-)regular model checking . . . . . . . . . . . . . . . . 119--143 Ahmed Bouajjani and Tayssir Touili Widening techniques for regular tree model checking . . . . . . . . . . . . . 145--165 Ahmed Bouajjani and Peter Habermehl and Adam Rogalewicz and Tomás Vojnar Abstract regular (tree) model checking 167--191 Bernard Boigelot Domain-specific regular acceleration . . 193--206 Giorgio Delzanno and Ahmed Rezine A lightweight regular model checking approach for parameterized systems . . . 207--222 Parosh Aziz Abdulla and Bengt Jonsson and Marcus Nilsson and Julien d'Orso and Mayank Saksena Regular model checking for LTL(MSO) . . 223--241
Oleg Sokolsky and Klaus Havelund and Insup Lee Introduction to the special section on runtime verification . . . . . . . . . . 243--247 Patrick O'Neil Meredith and Dongyun Jin and Dennis Griffith and Feng Chen and Grigore Rosu An overview of the MOP runtime verification framework . . . . . . . . . 249--289 Shaz Qadeer and Serdar Tasiran Runtime verification of concurrency-specific correctness criteria . . . . . . . . . . . . . . . . 291--305 Eric Bodden and Laurie Hendren The Clara framework for hybrid typestate analysis . . . . . . . . . . . . . . . . 307--326 Xiaowan Huang and Justin Seyster and Sean Callanan and Ketan Dixit and Radu Grosu and Scott A. Smolka and Scott D. Stoller and Erez Zadok Software monitoring with controllable overhead . . . . . . . . . . . . . . . . 327--347 Yli\`es Falcone and Jean-Claude Fernandez and Laurent Mounier What can you verify and enforce at runtime? . . . . . . . . . . . . . . . . 349--382
Alexandre Petrenko and Adenilso Simao and José Carlos Maldonado Model-based testing of software and systems: recent advances and challenges 383--386 Margus Veanes and Nikolaj Bjòrner Alternating simulation and IOCO . . . . 387--405 Yli\`es Falcone and Jean-Claude Fernandez and Thierry Jéron and Hervé Marchand and Laurent Mounier More testable properties . . . . . . . . 407--437 Christoph D. Gladisch Model generation for quantified formulas with application to test data generation 439--459 Silvia Regina Vergilio and Aurora Pozo and João Carlos Garcia Árias and Rafael da Veiga Cabral and Tiago Nobre Multi-objective optimization algorithms applied to the class integration and test order problem . . . . . . . . . . . 461--475
Ina Schaefer and Rick Rabiser and Dave Clarke and Lorenzo Bettini and David Benavides and Goetz Botterweck and Animesh Pathak and Salvador Trujillo and Karina Villela Software diversity: state of the art and perspectives . . . . . . . . . . . . . . 477--495 Andreas Pleuss and Goetz Botterweck Visualization of variability and configuration options . . . . . . . . . 497--510 Sven Jörges and Anna-Lena Lamprecht and Tiziana Margaria and Ina Schaefer and Bernhard Steffen A constraint-based variability modeling framework . . . . . . . . . . . . . . . 511--530 Reinhard Tartler and Julio Sincero and Christian Dietrich and Wolfgang Schröder-Preikschat and Daniel Lohmann Revealing and repairing configuration inconsistencies in large-scale system software . . . . . . . . . . . . . . . . 531--551 Patrick Heymans and Quentin Boucher and Andreas Classen and Arnaud Bourdoux and Laurent Demonceau A code tagging approach to software product line development: an application to satellite communication libraries . . 553--566 Peter Y. H. Wong and Elvira Albert and Radu Muschevici and José Proença and Jan Schäfer and Rudolf Schlatte The ABS tool suite: modelling, executing and analysing distributed adaptable object-oriented systems . . . . . . . . 567--588 Andreas Classen and Maxime Cordy and Patrick Heymans and Axel Legay and Pierre-Yves Schobbens Model checking software product lines with SNIP . . . . . . . . . . . . . . . 589--612 Wolfgang Heider and Rick Rabiser and Paul Grünbacher Facilitating the evolution of products in product line engineering by capturing and replaying configuration decisions 613--630
Zhiming Liu and Abhik Roychoudhury Relating software validation to technology trends . . . . . . . . . . . 631--638 Minxue Pan and Xuandong Li Timing analysis of MSC specifications with asynchronous concatenation . . . . 639--651 Chunqing Chen and Jun Sun and Yang Liu and Jin Song Dong and Manchun Zheng Formal modeling and validation of Stateflow diagrams . . . . . . . . . . . 653--671 Adriano Gomes and Alexandre Mota and Augusto Sampaio and Felipe Ferri and Edson Watanabe Constructive model-based analysis for safety assessment . . . . . . . . . . . 673--702 Alexandre David and Kim. G. Larsen and Axel Legay and Mikael H. Mòller and Ulrik Nyman and Anders P. Ravn and Arne Skou and Andrzej W\kasowski Compositional verification of real-time systems using Ecdar . . . . . . . . . . 703--720
Björn Lisper The ALL-TIMES project: introduction and overview . . . . . . . . . . . . . . . . 1--8 Nicholas Merriam and Peter Gliwa and Ian Broster Measurement and tracing methods for timing analysis . . . . . . . . . . . . 9--28 Reinhold Heckmann and Christian Ferdinand and Daniel Kästner and Stefana Nenova Architecture exploration and timing estimation during early design phases 29--39 Dietmar Schreiner and Gergö Barany and Markus Schordan and Jens Knoop Comparison of type-based and alias-based component recognition for embedded systems software . . . . . . . . . . . . 41--52 Björn Lisper and Andreas Ermedahl and Dietmar Schreiner and Jens Knoop and Peter Gliwa Practical experiences of applying source-level WCET flow analysis to industrial code . . . . . . . . . . . . 53--63 Nicholas Merriam and Björn Lisper Estimation of productivity increase for timing analysis tool chains . . . . . . 65--84
Parosh Aziz Abdulla and K. Rustan M. Leino Tools for software verification . . . . 85--88 Hubert Garavel and Frédéric Lang and Radu Mateescu and Wendelin Serwe CADP 2011: a toolbox for the construction and analysis of distributed processes . . . . . . . . . . . . . . . 89--107 Yih-Kuen Tsay and Ming-Hsien Tsai and Jinn-Shu Chang and Yi-Wen Chang and Chi-Shiang Liu Büchi Store: an open repository of $ \omega $-automata . . . . . . . . . . . 109--123 Abinoam P. Marques Jr. and Anders P. Ravn and Jirí Srba and Saleem Vighio Model-checking Web services business activity protocols . . . . . . . . . . . 125--147
Saddek Bensalem and Axel Legay and Marius Bozga Rigorous embedded design: challenges and perspectives . . . . . . . . . . . . . . 149--154 Kai Lampka and Simon Perathoner and Lothar Thiele Component-based system design: analytic real-time interfaces for state-based component implementations . . . . . . . 155--170 Jonas Rox and Rolf Ernst Compositional performance analysis with improved analysis techniques for obtaining viable end-to-end latencies in distributed embedded systems . . . . . . 171--187 Silviu S. Craciunas and Christoph M. Kirsch and Hannes Payer and Harald Röck and Ana Sokolova Temporal isolation in real-time systems: the VBS approach . . . . . . . . . . . . 189--209 Thi Thieu Hoa Le and Luigi Palopoli and Roberto Passerone and Yusi Ramadian Timed-automata based schedulability analysis for distributed firm real-time systems: a case study . . . . . . . . . 211--228 Ismail Assayad and Alain Girault and Hamoudi Kalla Tradeoff exploration between reliability, power consumption, and execution time for embedded systems . . 229--245 Oded Maler and Dejan Nickovi\'c Monitoring properties of analog and mixed-signal circuits . . . . . . . . . 247--268 Fred Houben and Georgeta Igna and Frits Vaandrager Modeling task systems using parameterized partial orders . . . . . . 269--286
Stefan Kowalewski and Anna Philippou and Jörg Brauer Model checking and abstract interpretation as building blocks of advanced program analysis techniques . . 287--289 Ashutosh Kumar Gupta and Rupak Majumdar and Andrey Rybalchenko From tests to proofs . . . . . . . . . . 291--303 Erion Plaku and Lydia E. Kavraki and Moshe Y. Vardi Falsification of LTL safety properties in hybrid systems . . . . . . . . . . . 305--320 Vineet Kahlon and Sriram Sankaranarayanan and Aarti Gupta Static analysis for concurrent programs with applications to data race detection 321--336 Viet Yen Nguyen and Theo C. Ruys Selected dynamic issues in software model checking . . . . . . . . . . . . . 337--362 Massimo Bombino and Patrizia Scandurra A model-driven co-simulation environment for heterogeneous systems . . . . . . . 363--374 Islam Abdelhalim and Steve Schneider and Helen Treharne An integrated framework for checking the behaviour of fUML models using CSP . . . 375--396
Rastislav Bodik and Barbara Jobstmann Algorithmic program synthesis: introduction . . . . . . . . . . . . . . 397--411 Martin Vechev and Eran Yahav and Greta Yorsh Abstraction-guided synthesis of synchronization . . . . . . . . . . . . 413--431 Saqib Sohail and Fabio Somenzi Safety first: a two-stage algorithm for the synthesis of reactive systems . . . 433--454 Viktor Kuncak and Mikaël Mayer and Ruzica Piskac and Philippe Suter Functional synthesis for linear arithmetic and sets . . . . . . . . . . 455--474 Armando Solar-Lezama Program sketching . . . . . . . . . . . 475--495 Saurabh Srivastava and Sumit Gulwani and Jeffrey S. Foster Template-based program verification and program synthesis . . . . . . . . . . . 497--518 Bernd Finkbeiner and Sven Schewe Bounded synthesis . . . . . . . . . . . 519--539 Emmanuel Filiot and Naiyong Jin and Jean-François Raskin Exploiting structure in LTL synthesis 541--561 Robert Könighofer and Georg Hofferek and Roderick Bloem Debugging formal specifications: a practical approach using model-based diagnosis and counterstrategies . . . . 563--583 Yashdeep Godhal and Krishnendu Chatterjee and Thomas A. Henzinger Synthesis of AMBA AHB from formal specification: a case study . . . . . . 585--601 Yoad Lustig and Moshe Y. Vardi Synthesis from component libraries . . . 603--618
Saddek Bensalem and Klaus Havelund and Andrea Orlandini Verification and validation meet planning and scheduling . . . . . . . . 1--12 Robert P. Goldman and Michael J. S. Pelican and David J. Musliner A loop acceleration technique to speed up verification of automatically generated plans . . . . . . . . . . . . 13--29 Jason Crampton and Michael Huth and Jim Huan-Pu Kuo Authorized workflow schemas: deciding realizability through $ \mathsf {LTL}(\mathsf {F}) $ model checking . . 31--48 Niloofar Razavi and Azadeh Farzan and Sheila A. McIlraith Generating effective tests for concurrent programs via AI automated planning techniques . . . . . . . . . . 49--65 Jason Snyder and Deepan Seeralan and Shereef Sayed and Jeffery Wilson and Carl B. Dietrich and Stephen H. Edwards and Jeffrey H. Reed Open source software-defined radio tools for education, research, and rapid prototyping . . . . . . . . . . . . . . 67--80 Jan Tobias Mühlberg and Gerald Lüttgen Symbolic object code analysis . . . . . 81--102 Hél\`ene Collavizza and Nguyen Le Vinh and Olivier Ponsini and Michel Rueher and Antoine Rollet Constraint-based BMC: a backjumping strategy . . . . . . . . . . . . . . . . 103--121
Cormac Flanagan and Barbara König Developments in automated verification techniques . . . . . . . . . . . . . . . 123--125 Ahmed Bouajjani and Michael Emmi Bounded phase analysis of message-passing programs . . . . . . . . 127--146 Fu Song and Tayssir Touili Pushdown model checking for malware detection . . . . . . . . . . . . . . . 147--173 Arlen Cox and Sriram Sankaranarayanan and Bor-Yuh Evan Chang A bit too precise? Verification of quantized digital filters . . . . . . . 175--190 Zhihao Jiang and Miroslav Pajic and Rajeev Alur and Rahul Mangharam Closed-loop verification of medical devices with model abstraction and refinement . . . . . . . . . . . . . . . 191--213
Jens Grabowski and Ina Schieferdecker and Andreas Ulrich History, status, and recent trends of the testing and test control notation version 3 (TTCN-3) . . . . . . . . . . . 215--225 Philip Makedonski and Jens Grabowski and Florian Philipp Quantifying the evolution of TTCN-3 as a language . . . . . . . . . . . . . . . . 227--246 Juergen Grossmann Testing hybrid systems with TTCN-3 embedded . . . . . . . . . . . . . . . . 247--267 Bernard Stepien and Liam Peyton Innovation and evolution in integrated web application testing with TTCN-3 . . 269--283 Benjamin Zeiss and Andras Kovacs and Nikolay Pakulin and Bogdan Stanca-Kaposta A conformance test suite for TTCN-3 tools . . . . . . . . . . . . . . . . . 285--294 Thomas Rings and Patrick Poglitsch and Stephan Schulz and Luca Serazio and Theofanis Vassiliou-Gioles A generic interoperability testing framework and a systematic development process for automated interoperability testing . . . . . . . . . . . . . . . . 295--313 Awny Alnusair and Tian Zhao and Gongjun Yan Rule-based detection of design patterns in program code . . . . . . . . . . . . 315--334
Tiziana Margaria and Zongyan Qiu and Hongli Yang Program verification and testing technologies . . . . . . . . . . . . . . 335--337 Huixing Fang and Jianqi Shi and Huibiao Zhu and Jian Guo and Kim Guldstrand Larsen and Alexandre David Formal verification and simulation for platform screen doors and collision avoidance in subway control systems . . 339--361 Cristian Gherghina and Cristina David and Shengchao Qin and Wei-Ngan Chin Expressive program verification via structured specifications . . . . . . . 363--380 João F. Ferreira and Cristian Gherghina and Guanhua He and Shengchao Qin and Wei-Ngan Chin Automated verification of the FreeRTOS scheduler in Hip/Sleek . . . . . . . . . 381--397 Yosr Jarraya and Mourad Debbabi Quantitative and qualitative analysis of SysML activity diagrams . . . . . . . . 399--419 Ender Yüksel and Hanne Riis Nielson and Flemming Nielson and Huibiao Zhu and Heqing Huang Quantitative modelling and analysis of a Chinese smart grid: a stochastic model checking case study . . . . . . . . . . 421--435 Hai-Feng Guo and Mahadevan Subramaniam Model-based test generation using extended symbolic grammars . . . . . . . 437--455
Falk Howar and Malte Isberner and Maik Merten and Bernhard Steffen and Dirk Beyer and Corina S. Pasareanu Rigorous examination of reactive systems 457--464 Bernhard Steffen and Malte Isberner and Stefan Naujokat and Tiziana Margaria and Maren Geske Property-driven benchmark generation: synthesizing programs of realistic structure . . . . . . . . . . . . . . . 465--479 Jaco van de Pol and Theo C. Ruys and Steven te Brinke Thoughtful brute-force attack of the RERS 2012 and 2013 Challenges . . . . . 481--491 Markus Schordan and Adrian Prantl Combining static analysis and state transition graphs for verification of event-condition-action systems in the RERS 2012 and 2013 Challenges . . . . . 493--505 Dirk Beyer and Andreas Stahlbauer BDD-based software verification . . . . 507--518 Jeremy Morse and Lucas Cordeiro and Denis Nicole and Bernd Fischer Applying symbolic bounded model checking to the 2012 RERS Greybox Challenge . . . 519--529 Oliver Bauer and Maren Geske and Malte Isberner Analyzing program behavior through active automata learning . . . . . . . . 531--542 Bernhard Steffen and Falk Howar and Malte Isberner and Stefan Naujokat and Tiziana Margaria Tailored generation of concurrent benchmarks . . . . . . . . . . . . . . . 543--558 Michael Felderer and Ina Schieferdecker A taxonomy of risk-based testing . . . . 559--568 Johannes Neubauer and Stephan Windmüller and Bernhard Steffen Risk-based testing via active continuous quality control . . . . . . . . . . . . 569--591 Gabriella Carrozza and Roberto Pietrantuono and Stefano Russo Dynamic test planning: a study in an industrial context . . . . . . . . . . . 593--607 Michael Felderer and Rudolf Ramler A multiple case study on risk-based testing in industry . . . . . . . . . . 609--625 Gencer Erdogan and Yan Li and Ragnhild Kobro Runde and Fredrik Seehusen and Ketil Stòlen Approaches for the combined use of risk analysis and testing: a systematic literature review . . . . . . . . . . . 627--642
Alessandro Fantechi and Francesco Flammini and Stefania Gnesi Formal methods for railway control systems . . . . . . . . . . . . . . . . 643--646 Alessio Ferrari and Giorgio O. Spagnolo and Giacomo Martelli and Simone Menabeni From commercial documents to system requirements: an approach for the engineering of novel CBTC solutions . . 647--667 Stefano Marrone and Francesco Flammini and Nicola Mazzocca and Roberto Nardone and Valeria Vittorini Towards Model-Driven V&V assessment of railway control systems . . . . . . . . 669--683 Phillip James and Faron Moller and Hoang Nga Nguyen and Markus Roggenbach and Steve Schneider and Helen Treharne Techniques for modelling and verifying railway interlockings . . . . . . . . . 685--711 Anne E. Haxthausen Automated generation of formal safety conditions from railway interlocking tables . . . . . . . . . . . . . . . . . 713--726 Stefan J. Galler and Bernhard K. Aichernig Survey on test data generation tools . . 727--751 Stefano Quer Model checking evaluation of airplane landing trajectories . . . . . . . . . . 753--773
Agneta Nilsson and Laura M. Castro and Samuel Rivas and Thomas Arts Assessing the effects of introducing a new software development process: a methodological description . . . . . . . 1--16 Alexandre David and Kim G. Larsen and Axel Legay and Ulrik Nyman and Louis-Marie Traonouez and Andrzej Wasowski Real-time specifications . . . . . . . . 17--45 Hong Yi Chen and Shaked Flur and Supratik Mukhopadhyay Termination proofs for linear simple loops . . . . . . . . . . . . . . . . . 47--57 Muhammad Shafique and Yvan Labiche A systematic review of state-based test tools . . . . . . . . . . . . . . . . . 59--76 Reza Pulungan and Holger Hermanns A construction and minimization service for continuous probability distributions 77--90 Daniel Lincke and Sibylle Schupp and Cezar Ionescu Functional prototypes for generic C++ libraries: a transformational approach based on higher-order, typed signatures 91--105 Peter Y. H. Wong and Richard Bubel and Frank S. de Boer and Miguel Gómez-Zamalloa and Stijn de Gouw and Reiner Hähnle and Karl Meinke and Muddassar Azam Sindhu Testing abstract behavioral specifications . . . . . . . . . . . . . 107--119
Yli\`es Falcone and Lenore D. Zuck Runtime verification: the application perspective . . . . . . . . . . . . . . 121--123 Sylvain Hallé and Jason Vallet and Raphaël Tremblay-Lessard On piggyback runtime monitoring of object-oriented programs . . . . . . . . 125--142 Klaus Havelund Rule-based runtime verification revisited . . . . . . . . . . . . . . . 143--170 Ayoub Nouri and Saddek Bensalem and Marius Bozga and Benoit Delahaye and Cyrille Jegourel and Axel Legay Statistical model checking QoS properties of systems with SBIP . . . . 171--185 Alexandre David and Kim G. Larsen and Axel Legay and Marius Mikucionis Schedulability of Herschel revisited using statistical model checking . . . . 187--199 Sébastien Salva and Stassia R. Zafimiharisoa APSET, an Android aPplication SEcurity Testing tool for detecting intent-based vulnerabilities . . . . . . . . . . . . 201--221 Farn Wang Model-checking fair dense-time systems with propositions and events . . . . . . 223--243
Michael Felderer and Basel Katt A process for mastering security evolution in the development lifecycle 245--250 Atle Refsdal and Bjòrnar Solhaug and Ketil Stòlen Security risk analysis of system changes exemplified within the oil and gas domain . . . . . . . . . . . . . . . . . 251--266 Jens Bürger and Jan Jürjens and Sven Wenzel Restoring security of evolving software models using graph transformation . . . 267--289 Dries Vanoverberghe and Frank Piessens Policy ignorant caller-side inline reference monitoring . . . . . . . . . . 291--303 Michael Felderer and Elizabeta Fourneret A systematic classification of security regression testing approaches . . . . . 305--319 Kenneth J. Turner and Paul S. Lambert Workflows for quantitative data analysis in the social sciences . . . . . . . . . 321--338 Grzegorz Anielak and Grzegorz Jakacki and Slawomir Lasota Incremental test case generation using bounded model checking: an application to automatic rating . . . . . . . . . . 339--349 Alexandre David and Kim G. Larsen and Axel Legay and Marius Mikucionis and Danny Bògsted Poulsen and Sean Sedwards Statistical model checking for biological systems . . . . . . . . . . . 351--367
Axel Legay and Mahesh Viswanathan Statistical model checking: challenges and perspectives . . . . . . . . . . . . 369--376 Daniël Reijsbergen and Pieter-Tjerk de Boer and Werner Scheinhardt and Boudewijn Haverkort On hypothesis testing for statistical model checking . . . . . . . . . . . . . 377--395 Alexandre David and Kim G. Larsen and Axel Legay and Marius Mikucionis and Danny Bògsted Poulsen Uppaal SMC tutorial . . . . . . . . . . 397--415 Nima Roohi and Mahesh Viswanathan Statistical model checking for unbounded until formulas . . . . . . . . . . . . . 417--427 Arnd Hartmanns and Mark Timmer Sound statistical model checking for MDP using partial order and confluence reduction . . . . . . . . . . . . . . . 429--456 Richard Lassaigne and Sylvain Peyronnet Approximate planning and verification for large Markov decision processes . . 457--467 Pedro D'Argenio and Axel Legay and Sean Sedwards and Louis-Marie Traonouez Smart sampling for lightweight verification of Markov decision processes . . . . . . . . . . . . . . . 469--484 Christian Ellen and Sebastian Gerwinn and Martin Fränzle Statistical model checking for stochastic hybrid systems involving nondeterminism over continuous domains 485--504 Paolo Ballarini Analysing oscillatory trends of discrete-state stochastic processes through HASL statistical model checking 505--526 Paolo Zuliani Statistical model checking for biological applications . . . . . . . . 527--536 Souymodip Chakraborty and Joost-Pieter Katoen and Falak Sher and Martin Strelec Modelling and statistical model checking of a microgrid . . . . . . . . . . . . . 537--554
Stefania Gnesi and Stan Jarzabek Special section on the 17th International Software Product Line Conference . . . . . . . . . . . . . . . 555--557 Holger Eichelberger and Klaus Schmid Mapping the design-space of textual variability modeling languages: a refined analysis . . . . . . . . . . . . 559--584 João Bosco Ferreira Filho and Olivier Barais Generating counterexamples of model-based software product lines . . . 585--600 Arne Haber and Katrin Hölldobler Systematic synthesis of delta modeling languages . . . . . . . . . . . . . . . 601--626 Julia Rubin and Krzysztof Czarnecki Cloned product variants: from ad-hoc to managed software product lines . . . . . 627--646
Marieke Huisman and Vladimir Klebanov VerifyThis 2012 . . . . . . . . . . . . 647--657 Bart Jacobs and Jan Smans and Frank Piessens Solving the VerifyThis 2012 challenges with VeriFast . . . . . . . . . . . . . 659--676 Gidon Ernst and Jörg Pfähler KIV: overview and VerifyThis competition 677--694 Duc Hoang and Yannick Moy and Angela Wallenburg SPARK 2014 and GNATprove . . . . . . . . 695--707 François Bobot and Jean-Christophe Filliâtre Let's verify this with Why3 . . . . . . 709--727 Daniel Bruns and Wojciech Mostowski Implementation-level verification of algorithms with KeY . . . . . . . . . . 729--744 Julian Tschannen and Carlo A. Furia AutoProof meets some verification challenges . . . . . . . . . . . . . . . 745--755 Stefan Blom and Marieke Huisman Witnessing the elimination of magic wands . . . . . . . . . . . . . . . . . 757--781
Mauro Pezzé and Jochen Wuttke Model-driven generation of runtime checks for system properties . . . . . . 1--19 Martijn Hendriks and Twan Basten A blueprint for system-level performance modeling of software-intensive embedded systems . . . . . . . . . . . . . . . . 21--40 Martin Wehrle and Sebastian Kupferschmid Downward pattern refinement for timed automata . . . . . . . . . . . . . . . . 41--56 Takeru Inoue and Hiroaki Iwashita and Jun Kawahara Graphillion: software library for very large sets of labeled graphs . . . . . . 57--66 Jan-David Quesel and Stefan Mitsch and Sarah Loos How to model and prove hybrid systems with \pkgKeYmaera: a tutorial on safety 67--91 Ammar Osaiweran and Mathijs Schuts Evaluating the effect of a lightweight formal technique in industry . . . . . . 93--108 Takuro Kutsuna and Yoshinao Ishii Abstraction and refinement of mathematical functions toward SMT-based test-case generation . . . . . . . . . . 109--120
Erika Ábrahám and Klaus Havelund Some recent advances in automated analysis . . . . . . . . . . . . . . . . 121--128 Gavin Lowe Concurrent depth-first search algorithms based on Tarjan's Algorithm . . . . . . 129--147 Thomas Gibson-Robinson and Philip Armstrong FDR3: a parallel refinement checker for CSP . . . . . . . . . . . . . . . . . . 149--167 Anton Wijs and Dragan Bosnacki Many-core on-the-fly model checking of safety properties using GPUs . . . . . . 169--185 Alessandro Armando and Roberto Carbone SATMC: a SAT-based model checker for security protocols, business processes, and security APIs . . . . . . . . . . . 187--204 Normann Decker and Martin Leucker and Daniel Thoma Monitoring modulo theories . . . . . . . 205--225 Christian von Essen and Dimitra Giannakopoulou Probabilistic verification and synthesis of the next generation airborne collision avoidance system . . . . . . . 227--243
Hüsnü Yenigün and Cemal Yilmaz and Andreas Ulrich Advances in test generation for testing software and systems . . . . . . . . . . 245--249 Natalia Kushik and Khaled El-Fakih and Nina Yevtushenko and Ana R. Cavalli On adaptive experiments for nondeterministic finite state machines 251--264 Wen-ling Huang and Jan Peleska Complete model-based equivalence class testing . . . . . . . . . . . . . . . . 265--283 João Pascoal Faria and Ana C. R. Paiva A toolset for conformance testing against UML sequence diagrams based on event-driven colored Petri nets . . . . 285--304 Hernán Ponce de León and Stefan Haar and Delphine Longuet Model-based testing for concurrent systems: unfolding-based test selection 305--318 Peter Schrammel and Tom Melham and Daniel Kroening Generating test case chains for reactive systems . . . . . . . . . . . . . . . . 319--334 Eduard P. Enoiu and Adnan Causevi\'c and Thomas J. Ostrand and Elaine J. Weyuker and Daniel Sundmark and Paul Pettersson Automated test generation using model checking: an industrial evaluation . . . 335--353
Ezio Bartocci and C. R. Ramakrishnan Preface of the special issue on Model Checking of Software . . . . . . . . . . 355--357 Nuno P. Lopes and José Monteiro Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic . . . . . . . . . 359--374 Divjyot Sethi and Muralidhar Talupur and Sharad Malik Model checking unbounded concurrent lists . . . . . . . . . . . . . . . . . 375--391 Kiran Adhikari and James Street and Chao Wang and Yang Liu and Shaojie Zhang Verifying a quantitative relaxation of linearizability via refinement . . . . . 393--407 Jonas Finnemann Jensen and Kim Guldstrand Larsen and Jirí Srba and Lars Kaerlund Oestergaard Efficient model-checking of weighted CTL with upper-bound constraints . . . . . . 409--426 Alfons Laarman and Elwin Pater and Jaco van de Pol and Henri Hansen Guard-based partial-order reduction . . 427--448 Sergiy Bogomolov and Alexandre Donzé and Goran Frehse and Radu Grosu and Taylor T. Johnson and Hamed Ladan and Andreas Podelski and Martin Wehrle Guided search for hybrid systems based on coarse-grained space abstractions . . 449--467
Parosh A. Abdulla and Giorgio Delzanno Parameterized verification . . . . . . . 469--473 Giorgio Delzanno A unified view of parameterized verification of abstract models of broadcast communication . . . . . . . . 475--493 Parosh Abdulla and Frédéric Haziza and Lukás Holík Parameterized verification through view abstraction . . . . . . . . . . . . . . 495--516 Zeinab Ganjei and Ahmed Rezine and Petru Eles and Zebo Peng Counting dynamically synchronizing processes . . . . . . . . . . . . . . . 517--534 Marco Montali and Diego Calvanese Soundness of data-aware, case-centric processes . . . . . . . . . . . . . . . 535--558 Silvio Ranise and Anh Truong and Riccardo Traverso Parameterized model checking for security policy analysis . . . . . . . . 559--573
Anna-Lena Lamprecht and Kenneth J. Turner Scientific workflows . . . . . . . . . . 575--580 Hervé Ménager and Matús Kalas and Kristoffer Rapacki and Jon Ison Using registries to integrate bioinformatics tools and services into workbench environments . . . . . . . . . 581--586 R. O. Sinnott and W. Voorsluys A scalable cloud-based system for data-intensive spatial analysis . . . . 587--605 Alfredo Bolt and Massimiliano de Leoni and Wil M. P. van der Aalst Scientific workflows for process mining: building blocks, scenarios, and implementation . . . . . . . . . . . . . 607--628 Anna-Lena Lamprecht and Bernhard Steffen and Tiziana Margaria Scientific workflows with the jABC framework . . . . . . . . . . . . . . . 629--651 Afshin Amighi and Pedro de Carvalho Gomes and Dilian Gurov and Marieke Huisman Provably correct control flow graphs from Java bytecode programs with exceptions . . . . . . . . . . . . . . . 653--684 Amar Kumar Gupta and Guy Edward Gallasch Equivalence class verification of the contract net protocol-extension . . . . 685--706
Bernhard Steffen The physics of software tools: SWOT analysis and vision . . . . . . . . . . 1--7 Alessio Lomuscio and Hongyang Qu and Franco Raimondi MCMAS: an open-source model checker for the verification of multi-agent systems 9--30 Víctor Rivera and Néstor Cataño and Tim Wahls and Camilo Rueda Code generation for Event-B . . . . . . 31--52 Adriana C. Damasceno and Patricia D. L. Machado and Wilkerson L. Andrade Testing real-time systems from compositional symbolic specifications 53--71 Kangfeng Ye and Jim Woodcock Model checking of state-rich formalism by linking to CSP\,$ \Vert $ \,B . . . . 73--96 Mikhail Y. R. Gadelha and Hussama I. Ismail and Lucas C. Cordeiro Handling loops in bounded model checking of C programs via $k$-induction . . . . 97--114 Philipp Zech and Philipp Kalb and Michael Felderer and Colin Atkinson and Ruth Breu Model-based regression testing by OCL 115--131
Frédéric Boniol and Virginie Wiels and Yamine A\"\it-Ameur and Klaus-Dieter Schewe The landing gear case study: challenges and experiments . . . . . . . . . . . . 133--140 Wen Su and Jean-Raymond Abrial Aircraft landing gear system: approaches with Event-B to the modeling of an industrial system . . . . . . . . . . . 141--166 Amel Mammar and Régine Laleau Modeling a landing gear system in Event-B . . . . . . . . . . . . . . . . 167--186 Lukas Ladenberger and Dominik Hansen and Harald Wiegard and Jens Bendisposto and Michael Leuschel Validation of the ABZ landing gear system using ProB . . . . . . . . . . . 187--203 Richard Banach The landing gear system in multi-machine Hybrid Event-B . . . . . . . . . . . . . 205--228 Ciprian Teodorov and Philippe Dhaussy and Luka Le Roux Environment-driven reachability for timed systems . . . . . . . . . . . . . 229--245 Paolo Arcaini and Angelo Gargantini and Elvinia Riccobene Rigorous development process of a safety-critical system: from ASM models to Java code . . . . . . . . . . . . . . 247--269
Steffen Herbold and Andreas Hoffmann Model-based testing as a service . . . . 271--279 Lom Messan Hillah and Ariele-Paolo Maesano and Fabio De Rosa and Fabrice Kordon and Pierre-Henri Wuillemin and Riccardo Fontanelli and Sergio Di Bona and Davide Guerri and Libero Maesano Automation and intelligent scheduling of distributed system functional testing 281--308 Steffen Herbold and Patrick Harms and Jens Grabowski Combining usage-based and model-based testing for service-oriented architectures in the industrial practice 309--324 M. A. Barcelona and L. García-Borgoñón and G. López-Nicolás Practical experiences in the usage of MIDAS in the logistics domain . . . . . 325--339 Yli\`es Falcone and Mohamad Jaber Fully automated runtime enforcement of component-based systems with formal and sound recovery . . . . . . . . . . . . . 341--365 Swen Jacobs and Roderick Bloem and Romain Brenguier and Rüdiger Ehlers and Timotheus Hell and Robert Könighofer and Guillermo A. Pérez and Jean-François Raskin and Leonid Ryzhyk and Ocan Sankur and Martina Seidl and Leander Tentrup and Adam Walker The first reactive synthesis competition (SYNTCOMP 2014) . . . . . . . . . . . . 367--390
Matthias Güdemann and Manuel Núñez Preface of the special issue on formal methods in industrial critical systems 391--393 Bogdan Aman and Gabriel Ciobanu Verification of critical systems described in real-time TiMo . . . . . . 395--408 Bernhard K. Aichernig and Klaus Hörmaier and Florian Lorber and Dejan Nickovi\'c and Stefan Tiran Require, test, and trace IT . . . . . . 409--426 Nasrine Damouche and Matthieu Martel and Alexandre Chapoutot Improving the numerical accuracy of programs by automatic transformation . . 427--448 Gal Katz and Doron Peled Synthesizing, correcting and improving code, using model checking-based genetic programming . . . . . . . . . . . . . . 449--464 Zoubeyr Farah and Yamine Ait-Ameur and Meriem Ouederni and Kamel Tari A correct-by-construction model for asynchronously communicating systems . . 465--485 Martijn Hendriks and Jacques Verriet and Twan Basten and Bart Theelen and Marco Brassé and Lou Somers Analyzing execution traces: critical-path analysis and distance analysis . . . . . . . . . . . . . . . . 487--510
Nir Piterman Advances in verification presented in TACAS'13 . . . . . . . . . . . . . . . . 511--515 Grigory Fedyukovich and Ondrej Sery and Natasha Sharygina Flexible SAT-based framework for incremental bounded upgrade checking . . 517--534 Isil Dillig and Thomas Dillig and Boyang Li and Ken McMillan and Mooly Sagiv Synthesis of circular compositional program proofs via abduction . . . . . . 535--547 Parosh Aziz Abdulla and Frédéric Haziza and Lukás Holík and Bengt Jonsson and Ahmed Rezine An integrated specification and verification technique for highly concurrent data structures for highly concurrent data structures . . . . . . . 549--563 Pierre Ganty and Radu Iosif and Filip Konecný Underapproximation of procedure summaries for integer programs . . . . . 565--584 Aleksandar S. Dimovski and Ahmad Salim Al-Sibahi and Claus Brabrand and Andrzej Wasowski Efficient family-based model checking via variability abstractions . . . . . . 585--603 Heinz Riener and Finn Haedicke and Stefan Frehse and Mathias Soeken and Daniel Große and Rolf Drechsler and Goerschwin Fey metaSMT: focus on your application and not on solver integration . . . . . . . 605--621 Tatsuya Abe and Toshiyuki Maeda A general model checking framework for various memory consistency models . . . 623--647
Christel Baier and Cesare Tinelli Some advances in tools and algorithms for the construction and analysis of systems . . . . . . . . . . . . . . . . 649--652 E. Renault and A. Duret-Lutz and F. Kordon and D. Poitrenaud Variations on parallel explicit emptiness checks for generalized Büchi automata . . . . . . . . . . . . . . . . 653--673 Tom van Dijk and Jaco van de Pol Sylvan: multi-core framework for decision diagrams . . . . . . . . . . . 675--696 Carlo A. Furia and Martin Nordio and Nadia Polikarpova and Julian Tschannen AutoProof: auto-active functional verification of object-oriented programs 697--716 Jean-Baptiste Jeannin and Khalil Ghorbal and Yanni Kouskoulas and Aurora Schmidt and Ryan Gardner and Stefan Mitsch and André Platzer A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system . . 717--741 Reza Meimandi Parizi and Abdul Azim Abdul Ghani and Sai Peck Lee and Saif Ur Rehman Khan RAMBUTANS: automatic AOP-specific test generation tool . . . . . . . . . . . . 743--761 Marieke Huisman and Vladimir Klebanov and Rosemary Monahan and Michael Tautschnig VerifyThis 2015 . . . . . . . . . . . . 763--771
Mohamad Jaber and Yli\`es Falcone and Kinan Dak-Al-Bab and John Abou-Jaoudeh and Mostafa El-Katerji A high-level modeling language for the efficient design, implementation, and testing of Android applications . . . . 1--18 Ily\`es Boukhari and Stéphane Jean and Idir Ait-Sadoune and Ladjel Bellatreche The role of user requirements in data repository design . . . . . . . . . . . 19--34 Vladimir Ulyantsev and Igor Buzhinsky and Anatoly Shalyto Exact finite-state machine identification from scenarios and temporal properties . . . . . . . . . . 35--55 Josie Holmes and Alex Groce and Jervis Pinto and Pranjal Mittal and Pooria Azimi and Kevin Kellar and James O'Brien TSTL: the template scripting testing language . . . . . . . . . . . . . . . . 57--78 Bardh Hoxha and Adel Dokhanchi and Georgios Fainekos Mining parametric temporal logic properties in model-based design for cyber-physical systems . . . . . . . . . 79--93 Vera Pantelic and Steven Postma and Mark Lawford and Monika Jaskolka and Bennett Mackenzie and Alexandre Korobkine and Marc Bender and Jeff Ong and Gordon Marks and Alan Wassyng Software engineering practices and Simulink: bridging the gap . . . . . . . 95--117
Radu Mateescu Recent advances in interactive and automated analysis . . . . . . . . . . . 119--123 Alexander Faithfull and Jesper Bengtson and Enrico Tassi and Carst Tankink Coqoon . . . . . . . . . . . . . . . . . 125--137 Gudmund Grov and Yuhui Lin The Tinker tool for graphical tactic development . . . . . . . . . . . . . . 139--155 Tom van Dijk and Jaco van de Pol Multi-core symbolic bisimulation minimisation . . . . . . . . . . . . . . 157--177 Joachim Klein and Christel Baier and Philipp Chrszon and Marcus Daum and Clemens Dubslaff and Sascha Klüppelholz and Steffen Märcker and David Müller Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic Büchi automata . . . . . . . . . . . . . . . . 179--194 Marta Kwiatkowska and David Parker and Clemens Wiltsche PRISM-games: verification and strategy synthesis for stochastic multi-player games with multiple objectives . . . . . 195--210 Peter W. V. Tran-Jòrgensen and Peter Gorm Larsen and Gary T. Leavens Automated translation of VDM to JML-annotated Java . . . . . . . . . . . 211--235
Maurice H. ter Beek and Stefania Gnesi and Alexander Knapp Formal methods for transport systems . . 237--241 Somsak Vanit-Anunchai Modelling and simulating a Thai railway signalling system using Coloured Petri Nets . . . . . . . . . . . . . . . . . . 243--262 Franco Mazzanti and Alessio Ferrari and Giorgio O. Spagnolo Towards formal methods diversity in railways: an experience report with seven frameworks . . . . . . . . . . . . 263--288 Vincenzo Ciancia and Stephen Gilmore and Gianluca Grilletti and Diego Latella and Michele Loreti and Mieke Massink Spatio-temporal model checking of vehicular movement in public transport systems . . . . . . . . . . . . . . . . 289--311 G. Cabodi and P. E. Camurati and C. Loiacono and M. Palena and P. Pasini and D. Patti and S. Quer To split or to group: from divide-and-conquer to sub-task sharing for verifying multiple properties in model checking . . . . . . . . . . . . . 313--325 Stefan Naujokat and Michael Lybecait and Dawid Kopetzki and Bernhard Steffen CINCO: a simplicity-driven approach to full generation of domain-specific graphical modeling tools . . . . . . . . 327--354
Maurice H. ter Beek and Stefania Gnesi and Alexander Knapp Formal methods and automated verification of critical systems . . . . 355--358 Johannes Leupolz and Alexander Knapp and Axel Habermaier and Wolfgang Reif Qualitative and quantitative analysis of safety-critical systems with . . . . . . 359--377 André de Matos Pedro and Jorge Sousa Pinto and David Pereira and Luís Miguel Pinho Runtime verification of autopilot systems using a fragment of MTL-$ \int $ 379--395 Mounir Chadli and Jin H. Kim and Kim G. Larsen and Axel Legay and Stefan Naujokat and Bernhard Steffen and Louis-Marie Traonouez High-level frameworks for the specification and verification of scheduling problems . . . . . . . . . . 397--422 Ning Ge and Eric Jenn and Nicolas Breton and Yoann Fonteneau Integrated formal verification of safety-critical software . . . . . . . . 423--440 Wen-ling Huang and Jan Peleska Model-based testing strategies and their (in)dependence on syntactic model representations . . . . . . . . . . . . 441--465 Hadrien Bride and Olga Kouchnarenko and Fabien Peureux and Guillaume Voiron Assessing SMT and CLP approaches for workflow nets verification . . . . . . . 467--491
Dragan Bosnacki and Anton Wijs Model checking: recent improvements and applications . . . . . . . . . . . . . . 493--497 María del Mar Gallardo and Pedro Merino and Laura Panizo and Alberto Salmerón Integrating river basin DSSs with model checking . . . . . . . . . . . . . . . . 499--514 Stefan Edelkamp and Christoph Greulich A case study of planning for smart factories . . . . . . . . . . . . . . . 515--528 Peter Gjòl Jensen and Kim Guldstrand Larsen and Jirí Srba Discrete and continuous strategies for timed-arc Petri net games . . . . . . . 529--546 Ehsan Khamespanah and Marjan Sirjani and Kirill Mechitov and Gul Agha Modeling and analyzing real-time wireless sensor and actuator networks using actors and model checking . . . . 547--561 Radu Mateescu and José Ignacio Requeno On-the-fly model checking for extended action-based probabilistic operators . . 563--587 Antti Valmari and Walter Vogler Fair testing and stubborn sets . . . . . 589--610
Marieke Huisman and Julia Rubin Software quality tools and techniques presented in FASE'17 . . . . . . . . . . 611--613 Andreas Müller and Stefan Mitsch and Werner Retschitzegger and Wieland Schwinger and André Platzer Tactical contract composition for hybrid system component verification . . . . . 615--643 Zheng Cheng and Massimo Tisi Slicing ATL model transformations for scalable deductive verification and fault localization . . . . . . . . . . . 645--663 Marcelo Uva and Pablo Ponzio and Germán Regis and Nazareno Aguirre and Marcelo F. Frias Automated workarounds from Java program specifications based on SAT solving . . 665--688 Jingyi Wang and Jun Sun and Qixia Yuan and Jun Pang Learning probabilistic models for model checking: an evolutionary approach and an empirical study . . . . . . . . . . . 689--704 Sven Schneider and Leen Lambers and Fernando Orejas Automated reasoning for attributed graph properties . . . . . . . . . . . . . . . 705--737 Irina Mariuca Asavoae and Mihail Asavoae and Adrián Riesco Slicing from formal semantics: Chisel --- a tool for generic program slicing 739--769
Dirk Beyer and Stefan Löwe and Philipp Wendler Reliable benchmarking: requirements and solutions . . . . . . . . . . . . . . . 1--29 Ezio Bartocci and Yli\`es Falcone and Borzoo Bonakdarpour and Christian Colombo and Normann Decker and Klaus Havelund and Yogi Joshi and Felix Klaedtke and Reed Milewicz and Giles Reger and Grigore Rosu and Julien Signoles and Daniel Thoma and Eugen Zalinescu and Yi Zhang First international Competition on Runtime Verification: rules, benchmarks, tools, and final results of CRV 2014 . . 31--70 Andreas Fellner and Bruno Woltzenlogel Paleo Greedy pebbling for proof space compression . . . . . . . . . . . . . . 71--86 Stanley Bak and Omar Ali Beg and Sergiy Bogomolov and Taylor T. Johnson and Luan Viet Nguyen and Christian Schilling Hybrid automata: from verification to implementation . . . . . . . . . . . . . 87--104 Stanislav Dashevskyi and Daniel Ricardo dos Santos and Fabio Massacci and Antonino Sabetta TestREx: a framework for repeatable exploits . . . . . . . . . . . . . . . . 105--119
Maxime Routhier and Richard St-Denis A qualitative assessment of $ \alpha $ Rby in the perspective of the supervisory control theory . . . . . . . 121--141 Fadi A. Zaraket and Mohamad Jaber and Mohamad Noureddine and Yli\`es Falcone From high-level modeling toward efficient and trustworthy circuits . . . 143--163 Chunyan Fu and Kougen Zheng Formal modeling and analysis of ad hoc Zone Routing Protocol in Event-B . . . . 165--181 Gervasio Pérez and Sergio Yovine Formal specification and implementation of an automated pattern-based parallel-code generation framework . . . 183--202 Étienne André What's decidable about parametric timed automata? . . . . . . . . . . . . . . . 203--219 Philipp Zech and Michael Felderer and Ruth Breu Knowledge-based security testing of web applications by logic programming . . . 221--246
Hakan Erdogmus and Klaus Havelund Introduction to Selected Papers from SPIN 2017 . . . . . . . . . . . . . . . 247--248 Jinru Hua and Yushan Zhang and Yuqun Zhang and Sarfraz Khurshid EdSketch: execution-driven sketching for Java . . . . . . . . . . . . . . . . . . 249--265 Daniel Ratiu and Andreas Ulrich An integrated environment for Spin-based C code checking . . . . . . . . . . . . 267--286 Michalis Kokologiannakis and Konstantinos Sagonas Stateless model checking of the Linux kernel's read-copy update (RCU) . . . . 287--306 Vincent Bloemen and Alexandre Duret-Lutz and Jaco van de Pol Model checking with generalized Rabin and Fin-less automata . . . . . . . . . 307--324 John Fearnley and Sanjay Jain and Bart de Keijzer and Sven Schewe and Frank Stephan and Dominik Wojtczak An ordered approach to solving parity games in quasi-polynomial time and quasi-linear space . . . . . . . . . . . 325--349 Esmaeel Nikravan and Saeed Parsa A reasoning-based approach to dynamic domain reduction in test data generation 351--364
Pavel Parízek and Ondrej Lhoták Fast detection of concurrency errors by state space traversal with randomization and early backtracking . . . . . . . . . 365--400 Amit Gurung and Rajarshi Ray and Ezio Bartocci and Sergiy Bogomolov and Radu Grosu Parallel reachability analysis of hybrid systems in XSpeed . . . . . . . . . . . 401--423 Julien Botella and Jean-François Capuron and Frédéric Dadeau and Elizabeta Fourneret and Bruno Legeard and Florence Schadle Complementary test selection criteria for model-based testing of security components . . . . . . . . . . . . . . . 425--448 Simon Busard and Charles Pecheur and Hongyang Qu and Franco Raimondi Comparing approaches for model-checking strategies under imperfect information and fairness constraints . . . . . . . . 449--469 Matthew F. Tennyson ASAP: a Source Code Authorship Program 471--484
Martin Hentschel and Richard Bubel and Reiner Hähnle The Symbolic Execution Debugger (SED): a platform for interactive symbolic execution, debugging, verification and more . . . . . . . . . . . . . . . . . . 485--513 Martin Becker and Ravindra Metta and R. Venkatesh and Samarjit Chakraborty Scalable and precise estimation and debugging of the worst-case execution time for analysis-friendly processors: a comeback of model checking . . . . . . . 515--543 Vladimir Herdt and Hoang M. Le and Daniel Große and Rolf Drechsler Combining sequentialization-based verification of multi-threaded C programs with symbolic Partial Order Reduction . . . . . . . . . . . . . . . 545--565 Thomas Gibson-Robinson and Gavin Lowe Symmetry reduction in CSP model checking 567--605
Maurice H. ter Beek and Axel Legay Quantitative variability modelling and analysis . . . . . . . . . . . . . . . . 607--612 Lars Luthmann and Timo Gerecht and Malte Lochau Sampling strategies for product lines with unbounded parametric real-time constraints . . . . . . . . . . . . . . 613--633 Maxime Cordy and Axel Legay Verification and abstraction of real-time variability-intensive systems 635--649 Linda Herrmann and Martin Küttler and Tobias Stumpf and Christel Baier and Hermann Härtig and Sascha Klüppelholz Configuration of inter-process communication with probabilistic model checking . . . . . . . . . . . . . . . . 651--666 Uli Fahrenberg and Axel Legay Quantitative properties of featured automata . . . . . . . . . . . . . . . . 667--677 Davide Basile Applying supervisory control synthesis to priced featured automata and energy problems . . . . . . . . . . . . . . . . 679--689 Ferruccio Damiani and Michael Lienhardt and Luca Paolini Automatic refactoring of delta-oriented SPLs to remove-free form and replace-free form . . . . . . . . . . . 691--707
Alessandra Russo and Andy Schürr Model-based software quality assurance tools and techniques presented at FASE 2018 . . . . . . . . . . . . . . . . . . 1--2 Fotios Gioulekas and Peter Poplavko and Panagiotis Katsaros and Saddek Bensalem and Pedro Palomo Correct-by-construction model-based design of reactive streaming software for multi-core embedded systems . . . . 3--32 Fotios Gioulekas and Peter Poplavko and Panagiotis Katsaros and Saddek Bensalem and Pedro Palomo Correction to: Correct-by-construction model-based design of reactive streaming software for multi-core embedded systems 33--34 Aleksandar S. Dimovski CTL$^\star $ family-based model checking using variability abstractions and modal transition systems . . . . . . . . . . . 35--55 Oszkár Semeráth and Rebeka Farkas and Gábor Bergmann and Dániel Varró Diversity of graph models and graph generators in mutation testing . . . . . 57--78 Márton Búr and Gábor Szilágyi and András Vörös and Dániel Varró Distributed graph queries over models@run.time for runtime monitoring of cyber-physical systems . . . . . . . 79--102
María del Mar Gallardo and Pedro Merino Introduction to the Special Issue devoted to SPIN 2018 . . . . . . . . . . 103--104 Laura Panizo and Almudena Díaz and Bruno García Model-based testing of apps in real network scenarios . . . . . . . . . . . 105--114 Marek Chalupa and Jan Strejcek and Martina Vitovská Joint forces for memory safety checking revisited . . . . . . . . . . . . . . . 115--133 Tim Lange and Martin R. Neuhäußer and Thomas Noll and Joost-Pieter Katoen IC3 software model checking . . . . . . 135--161 Bernard Berthomieu and Didier Le Botlan and Silvano Dal Zilio Counting Petri net markings from reduction equations . . . . . . . . . . 163--181 Hamzeh M. Allawi and Waref Al Manaseer and Mohammad Al Shraideh A greedy particle swarm optimization (GPSO) algorithm for testing real-world smart card applications . . . . . . . . 183--194 Fabrizio Banci Buonamici and Gina Belmonte and Vincenzo Ciancia and Diego Latella and Mieke Massink Spatial logics and model checking for medical imaging . . . . . . . . . . . . 195--217 Hana Mkaouar and Bechir Zalila and Jérôme Hugues and Mohamed Jmaiel A formal approach to AADL model-based software engineering . . . . . . . . . . 219--247
Michael Butler and Thai Son Hoang and Alexander Raschke and Klaus Reichl Introduction to special section on the ABZ 2018 case study: Hybrid ERTMS/ETCS Level 3 . . . . . . . . . . . . . . . . 249--255 Jean-Raymond Abrial The ABZ-2018 case study with Event-B . . 257--264 Paolo Arcaini and Jan Kofron and Pavel Jezek Validation of the Hybrid ERTMS/ETCS Level 3 using Spin . . . . . . . . . . . 265--279 Alcino Cunha and Nuno Macedo Validating the Hybrid ERTMS/ETCS Level 3 concept with Electrum . . . . . . . . . 281--296 Dana Dghaym and Mohammadsadegh Dalvandi and Michael Poppleton and Colin Snook Formalising the Hybrid ERTMS Level 3 specification in iUML-B and Event-B . . 297--313 Dominik Hansen and Michael Leuschel and Philipp Körner and Sebastian Krings and Thomas Naulin and Nader Nayeri and David Schneider and Frank Skowron Validation and real-life demonstration of ETCS hybrid level 3 principles using a formal B model . . . . . . . . . . . . 315--332 Amel Mammar and Marc Frappier and Steve Jeffrey Tueno Fotso and Régine Laleau A formal refinement-based analysis of the hybrid ERTMS/ETCS Level 3 standard 333--347 Steve Jeffrey Tueno Fotso and Marc Frappier and Régine Laleau and Amel Mammar Modeling the hybrid ERTMS/ETCS Level 3 standard using a formal requirements engineering approach . . . . . . . . . . 349--363
Ali Parsai and Serge Demeyer Comparing mutation coverage against branch coverage in an industrial setting 365--388 Rocco De Nicola and Stefan Jähnichen and Martin Wirsing Rigorous engineering of collective adaptive systems: special section . . . 389--397 Dhaminda B. Abeywickrama and Nicola Bicocchi and Franco Zambonelli The SOTA approach to engineering collective adaptive systems . . . . . . 399--415 Houssem Ben Mahfoudh and Giovanna Di Marzo Serugendo and Nabil Abdennadher Learning-based coordination model for spontaneous self-composition of reliable services in a distributed system . . . . 417--436 Rocco De Nicola and Alessandro Maggi and Joseph Sifakis The DReAM framework for dynamic reconfigurable architecture modelling: theory and applications . . . . . . . . 437--455 Thomas Gabor and Andreas Sedlmeier and Claudia Linnhoff-Popien The scenario coevolution paradigm: adaptive quality assurance for adaptive systems . . . . . . . . . . . . . . . . 457--476 Yehia Abd Alrahman and Giulio Garbi A distributed API for coordinating AbC programs . . . . . . . . . . . . . . . . 477--496 Tomas Bures and Ilias Gerostathopoulos and Jan Kofron A language and framework for dynamic component ensembles in smart systems . . 497--509 Rima Al Ali and Tomas Bures and Jiri Vinarek Toward autonomically composable and context-dependent access control specification through ensembles . . . . 511--522
Milan Ceska and Vojtech Havlena and Tomás Vojnar Approximate reduction of finite automata for high-speed network intrusion detection . . . . . . . . . . . . . . . 523--539 Elvio G. Amparore and Susanna Donatelli and Gianfranco Ciardo Variable order metrics for decision diagrams in system verification . . . . 541--562 Fabrizio Biondi and Thomas Given-Wilson and Axel Legay Introduction to the special issue for SPIN 2019 . . . . . . . . . . . . . . . 563--564 Patrick Metzler and Neeraj Suri and Georg Weissenbacher Extracting safe thread schedules from incomplete model checking results . . . 565--581 Richard DeFrancisco and Shenghsun Cho and Scott A. Smolka Swarm model checking on the GPU . . . . 583--599 Muhammad Usman and Wenxi Wang and Sarfraz Khurshid A study of learning likely data structure properties using machine learning models . . . . . . . . . . . . 601--615 Farnaz Yousefi and Ehsan Khamespanah and Ali Movaghar VeriVANca framework: verification of VANETs by property-based message passing of actors in Rebeca with inheritance . . 617--633 Sòren Enevoldsen and Kim G. Larsen and Jirí Srba Dependency graphs with applications to verification . . . . . . . . . . . . . . 635--654
Yi Li and Wenyuan Wu and Yong Feng On ranking functions for single-path linear-constraint loops . . . . . . . . 655--666 Luis Diogo Couto and Peter W. V. Tran-Jòrgensen and Peter Gorm Larsen Enabling continuous integration in a formal methods setting . . . . . . . . . 667--683 Dirk Beyer and Marieke Huisman Tools for the construction and analysis of systems . . . . . . . . . . . . . . . 685--687 Iulia Dragomir and Viorel Preoteasa and Stavros Tripakis The Refinement Calculus of Reactive Systems Toolset . . . . . . . . . . . . 689--708 Alexander J. Summers and Peter Müller Automating deductive verification for weak-memory programs (extended version) 709--728 Bernd Finkbeiner and Christopher Hahn and Leander Tentrup Efficient monitoring of hyperproperties using prefix trees . . . . . . . . . . . 729--740 Dejan Nickovi\'c and Olivier Lebeltel and Dogan Ulus AMT 2.0: qualitative and quantitative trace analysis with extended signal temporal logic . . . . . . . . . . . . . 741--758 Carlos E. Budde and Pedro R. D'Argenio and Sean Sedwards An efficient statistical model checker for nondeterminism and rare events . . . 759--780
Georgios Giantamidis and Stavros Tripakis and Stylianos Basagiannis Learning Moore machines from input--output traces . . . . . . . . . . 1--29 Chris Alvin and Brian Peterson and Supratik Mukhopadhyay Static generation of UML sequence diagrams . . . . . . . . . . . . . . . . 31--53 Yue Yuan and Yi Li and Wenchang Shi Detecting multiphase linear ranking functions for single-path linear-constraint loops . . . . . . . . 55--67 Florian Kammüller and Axel Legay and Stefano Schivo Masterminding change by combining secure system design with security risk assessment . . . . . . . . . . . . . . . 69--70 Pietro Ferrara and Amit Kr Mandal and Fausto Spoto Static analysis for discovering IoT vulnerabilities . . . . . . . . . . . . 71--88 René Rydhof Hansen and Kim Guldstrand Larsen and Danny Bògsted Poulsen ADTLang: a programming language approach to attack defense trees . . . . . . . . 89--104 Vladimir Shakhov and Insoo Koo Graph-based technique for survivability assessment and optimization of IoT applications . . . . . . . . . . . . . . 105--114
Omar M. Alhawi and Herbert Rocha and Eddie Batista Verification and refutation of C programs based on $k$-induction and invariant inference . . . . . . . . . . 115--135 Raphaël Khoury and Sylvain Hallé and Yannick Lebrun Automata-based monitoring for LTL-FO$^+$ 137--154 Martin Leucker and Christian Colombo Preface . . . . . . . . . . . . . . . . 155--156 Felipe Gorostiaga and César Sánchez Stream runtime verification of real-time event streams with the Striver language 157--183 Joshua Schneider and David Basin and Dmitriy Traytel Scalable online first-order monitoring 185--208 Giles Reger and David Rydeheard From parametric trace slicing to rule systems . . . . . . . . . . . . . . . . 209--228 Patricia Bouyer and Léo Henry and Nicolas Markey Diagnosing timed automata using timed markings . . . . . . . . . . . . . . . . 229--253 Yli\`es Falcone and Srdan Krsti\'c and Dmitriy Traytel A taxonomy for classifying runtime verification tools . . . . . . . . . . . 255--284
Reiner Hähnle and Wil van der Aalst Automated model analysis tools and techniques presented at FASE 2019 . . . 285--287 Artur Boronat Incremental execution of rule-based model transformation . . . . . . . . . . 289--311 Dirk Beyer and Marie-Christine Jakobs Cooperative verifier-based testing with CoVeriTest . . . . . . . . . . . . . . . 313--333 Lars Fritsche and Jens Kosiol and Gabriele Taentzer Avoiding unnecessary information loss: correct and efficient model synchronization based on triple graph grammars . . . . . . . . . . . . . . . . 335--368 Sven Schneider and Leen Lambers and Fernando Orejas A logic-based incremental approach to graph repair featuring delta preservation . . . . . . . . . . . . . . 369--410 Sven Schneider and Maria Maximova and Holger Giese Formal testing of timed graph transformation systems using metric temporal graph logic . . . . . . . . . . 411--488 Paul Dubrulle and Nikolai Kosmatov and Arnault Lapitre \pkgPolyGraph: a data flow model with frequency arithmetic . . . . . . . . . . 489--517 Paul Dubrulle and Nikolai Kosmatov and Arnault Lapitre Correction to: \pkgPolyGraph: a data flow model with frequency arithmetic . . 519--519
Markus Frohme and Bernhard Steffen Compositional learning of mutually recursive procedural systems . . . . . . 521--543 Bernd Finkbeiner and Leonardo Mariani Introduction to the special issue of the 19th International Conference on Runtime Verification . . . . . . . . . . . . . . 545--546 Klaus Havelund and Doron Peled An extension of first-order LTL with rules with application to runtime verification . . . . . . . . . . . . . . 547--563 Dejan Nickovi\'c and Xin Qin and Jyotirmoy Deshmukh Specifying and detecting temporal patterns with shape expressions . . . . 565--577 Sean Kauffman and Klaus Havelund and Sebastian Fischmeister What can we monitor over unreliable channels? . . . . . . . . . . . . . . . 579--600 Luca Aceto and Ian Cassar and Anna Ingólfsdóttir Comparing controlled system synthesis and suppression enforcement . . . . . . 601--614 Luca Bortolussi and Francesca Cairoli and Scott D. Stoller Neural predictive monitoring and a comparison of frequentist and Bayesian approaches . . . . . . . . . . . . . . . 615--640 Saeid Tizpaz-Niari and Pavol Cerný and Ashutosh Trivedi Quantitative estimation of side-channel leaks with neural networks . . . . . . . 641--654
Dawid Kopetzki and Michael Lybecait and Bernhard Steffen Towards language-to-language transformation . . . . . . . . . . . . . 655--677 Simon Bliudze and Panagiotis Katsaros and Martin Wirsing On methods and tools for rigorous system design . . . . . . . . . . . . . . . . . 679--684 Christos Grompanopoulos and Antonios Gouglidis and Anastasia Mavridou Specifying and verifying usage control models and policies in TLA$^+$ . . . . . 685--700 Rim El Ballouli and Saddek Bensalem and Joseph Sifakis Programming dynamic reconfigurable systems . . . . . . . . . . . . . . . . 701--719 Pujie Han and Zhengjun Zhai and Ulrik Nyman Model-based optimization of ARINC-653 partition scheduling . . . . . . . . . . 721--740 S. Blom and S. Darabi and M. Safari Correct program parallelisations . . . . 741--763 Alexios Lekidis and Panagiotis Katsaros Energy characterization of IoT systems through design aspect monitoring . . . . 765--781 Ezio Bartocci and Niveditha Manjunath and Dejan Nickovi\'c CPSDebug: Automatic failure explanation in CPS models . . . . . . . . . . . . . 783--796 Nathalie Bertrand and Igor Konnov and Josef Widder Verification of randomized consensus algorithms under round-rigid adversaries 797--821 Nathalie Bertrand and Igor Konnov and Josef Widder Correction to: Verification of randomized consensus algorithms under round-rigid adversaries . . . . . . . . 823--823 Parosh Aziz Abdulla and Frédéric Haziza and Ahmed Rezine Correction to: An integrated specification and verification technique for highly concurrent data structures 825--825 Jan-David Quesel and Stefan Mitsch and André Platzer Correction to: How to model and prove hybrid systems with \pkgKeYmaera: a tutorial on safety . . . . . . . . . . . 827--827
Dirk Beyer and Marieke Huisman TOOLympics I: Competition on software testing . . . . . . . . . . . . . . . . 829--832 Dirk Beyer First international competition on software testing . . . . . . . . . . . . 833--846 Marie-Christine Jakobs \pkgCoVeriTest: interleaving value and predicate analysis for test-case generation . . . . . . . . . . . . . . . 847--851 Sebastian Ruland and Malte Lochau and Andy Schürr \pkgCPA/Tiger-MGP: test-goal set partitioning for efficient multi-goal test-suite generation . . . . . . . . . 853--856 Mikhail R. Gadelha and Rafael S. Menezes and Lucas C. Cordeiro \pkgESBMC 6.1: automated test case generation using bounded model checking 857--861 Caroline Lemieux and Koushik Sen \pkgFairFuzz-TC: a fuzzer targeting rare branches . . . . . . . . . . . . . . . . 863--866 Cristian Cadar and Martin Nowack \pkgKLEE symbolic execution engine in 2019 . . . . . . . . . . . . . . . . . . 867--870 Thomas Lemberger Plain random test generation with \pkgPRTest . . . . . . . . . . . . . . . 871--873 Marek Chalupa and Martina Vitovská and Jan Strejcek \pkgSymbiotic 6: generating test cases by slicing and symbolic execution . . . 875--877 Dirk Beyer and Marieke Huisman and Bernhard Steffen TOOLympics II: competitions on formal methods . . . . . . . . . . . . . . . . 879--881 Claire Dross and Carlo A. Furia and Peter Müller VerifyThis 2019: a program verification competition . . . . . . . . . . . . . . 883--893 Mihaela Sighireanu SL-COMP: competition of solvers for separation logic . . . . . . . . . . . . 895--903 Aart Middeldorp and Julian Nagele and Kiraku Shintani CoCo 2019: report on the eighth confluence competition . . . . . . . . . 905--916 Falk Howar and Marc Jasper and Bernhard Steffen The RERS challenge: towards controllable and scalable benchmark synthesis . . . . 917--930 Fabrice Kordon and Lom Messan Hillah and Emmanuel Paviot-Adet Study of the efficiency of model checking techniques using results of the MCC from 2015 To 2019 . . . . . . . . . 931--952
Lukás Charvát and Ales Smrcka and Tomás Vojnar Utilizing parametric systems for detection of pipeline hazards . . . . . 1--28 Tomás Vojnar and Lijun Zhang Tools and algorithms for the construction and analysis of systems: a special issue for TACAS 2019 . . . . . . 29--31 Ilina Stoilkovska and Igor Konnov and Florian Zuleger Verifying safety of synchronous fault-tolerant algorithms by bounded model checking . . . . . . . . . . . . . 33--48 Sòren Enevoldsen and Kim Guldstrand Larsen and Jirí Srba Extended abstract dependency graphs . . 49--65 Petar Vukmirovi\'c and Jasmin Blanchette and Stephan Schulz Extending a brainiac prover to lambda-free higher-order logic . . . . . 67--87 Junaid Babar and Gianfranco Ciardo and Andrew Miner CESRBDDs: binary decision diagrams with complemented edges and edge-specified reductions . . . . . . . . . . . . . . . 89--109 Martin Blicha and Antti E. J. Hyvärinen and Natasha Sharygina Using linear algebra in decomposition of Farkas interpolants . . . . . . . . . . 111--125
Alexandre Vernotte and Aymeric Cretin and Fabien Peureux A domain-specific language to design false data injection tests for air traffic control systems . . . . . . . . 127--158 Antoine El-Hokayem and Yli\`es Falcone Bringing runtime verification home: a case study on the hierarchical monitoring of smart homes using decentralized specifications . . . . . . 159--181 Marlon Dumas and Luciano García-Bañuelos and Maksym Yerokhin Multi-level privacy analysis of business processes: the Pleak toolset . . . . . . 183--203 Paul-Antoine Arras and Anastasios Andronidis and Cristian Cadar SaBRe: load-time selective binary rewriting . . . . . . . . . . . . . . . 205--223 Hassna Louadah and Yvan Labiche Interface control document modeling with Citrus (avionics systems interfaces) . . 225--245 Lorenzo Bettini and Davide Di Ruscio and Alfonso Pierantonio Supporting safe metamodel evolution with edelta . . . . . . . . . . . . . . . . . 247--260 Per Erik Strandberg and Wasif Afzal and Daniel Sundmark Software test results exploration and visualization with continuous integration and nightly testing . . . . 261--285 Gavin Lowe Parameterized verification of systems with component identities, using view abstraction . . . . . . . . . . . . . . 287--324
Maurice H. ter Beek and Kim G. Larsen and Tim A. C. Willemse Formal methods and tools for industrial critical systems . . . . . . . . . . . . 325--330 Norman Weik and Matthias Volk and Nils Nießen DFT modeling approach for operational risk assessment of railway infrastructure . . . . . . . . . . . . . 331--350 Davide Basile and Maurice H. ter Beek and Axel Legay Exploring the ERTMS/ETCS full moving block specification: an experience with formal methods . . . . . . . . . . . . . 351--370 Yanni Kouskoulas and T. J. Machado and Joshua Brulé Envelopes and waves: safe multivehicle collision avoidance for horizontal non-deterministic turns . . . . . . . . 371--394 Rong Gu and Peter G. Jensen and Kristina Lundqvist Verifiable strategy synthesis for multiple autonomous agents: a scalable approach . . . . . . . . . . . . . . . . 395--414 Benjamin Binder and Mihail Asavoae and Mathieu Jan Formal modeling and verification for amplification timing anomalies in the superscalar TriCore architecture . . . . 415--440 Olav Bunte and Louis C. M. van Gool and Tim A. C. Willemse Formal verification of OIL component specifications using mCRL2 . . . . . . . 441--472 Samuel Huang and Rance Cleaveland Temporal-logic query checking over finite data streams . . . . . . . . . . 473--492 Petr Rockai and Jirí Barnat DivSIM, an interactive simulator for LLVM bitcode . . . . . . . . . . . . . . 493--510
Elahe Habibi and Seyed-Hasan Mirian-Hosseinabadi Generating test as a web service (TaaWS) through a method-based attribute grammar 511--527 Sebastien Salva and Elliott Blot Learning of behavioural models and dependency graphs for communicating systems with CkTailv2 . . . . . . . . . 529--548 H. M. W. Verbeek The Log Skeleton Visualizer in ProM 6.9 549--561 Christoffer Olling Back and Tijs Slaats and Thomas Troels Hildebrandt and Morten Marquard DisCoveR: accurate and efficient discovery of declarative process models 563--587 Christian Hensel and Sebastian Junges and Joost-Pieter Katoen and Tim Quatmann and Matthias Volk The probabilistic model checker Storm 589--610 Axel Legay and Tiziana Margaria Tools and algorithms for the construction and analysis of systems: a special issue for TACAS 2017 . . . . . . 611--612 Pedro Antonino and Thomas Gibson-Robinson and A. W. Roscoe Approximate verification of concurrent systems using token structures and invariants . . . . . . . . . . . . . . . 613--633 Javier Esparza and Jan K\vret\'ìnský and Jean-François Raskin and Salomon Sickert From linear temporal logic and limit-deterministic Büchi automata to deterministic parity automata . . . . . 635--659 Dirk Beyer and Stefan Löwe and Philipp Wendler Correction to: Reliable benchmarking: requirements and solutions . . . . . . . 661--661
Armin Biere and David Parker Tools and algorithms for the construction and analysis of systems: a special issue for TACAS 2020 . . . . . . 663--665 Hadar Frenkel and Orna Grumberg and Corina S. P\uas\uareanu and Sarai Sheinvald Assume, guarantee or repair: a regular framework for non regular properties . . 667--689 Florian Frohn and Carsten Fuhs A calculus for modular loop acceleration and non-termination proofs . . . . . . . 691--715 Benedikt Becker and Nicolas Jeannerod and Claude Marché and Yann Régis-Gianas and Mihaela Sighireanu and Ralf Treinen The CoLiS platform for the analysis of maintainer scripts in Debian software packages . . . . . . . . . . . . . . . . 717--733 Thomas Neele and Tim A. C. Willemse and Wieger Wesselink and Antti Valmari Partial-order reduction for parity games and parameterised Boolean equation systems . . . . . . . . . . . . . . . . 735--756 Ruben Hamers and Erik Horlings and Sung-Shik Jongmans The Discourje project: run-time verification of communication protocols in Clojure . . . . . . . . . . . . . . . 757--782 Hans-Dieter A. Hiep and Olaf Maathuis and Jinting Bian and Frank S. de Boer and Stijn de Gouw Verifying OpenJDK's LinkedList using KeY (extended paper) . . . . . . . . . . . . 783--802 Thom Badings and Murat Cubuktepe and Nils Jansen and Sebastian Junges and Joost-Pieter Katoen and Ufuk Topcu Scenario-based verification of uncertain parametric MDPs . . . . . . . . . . . . 803--819 Carlos E. Budde and Pedro R. D'Argenio and Raúl E. Monti and Mariëlle Stoelinga Analysis of non-Markovian repairable fault trees through rare event simulation . . . . . . . . . . . . . . . 821--841 Supratik Chakraborty and Ashutosh Gupta and Divyesh Unadkat Full-program induction: verifying array programs sans loop invariants . . . . . 843--888
Mawal A. Mohammed and Jameleddine Hassine and Mohammad Alshayeb GSDetector: a tool for automatic detection of bad smells in GRL goal models . . . . . . . . . . . . . . . . . 889--910 Jaehun Lee and Kyungmin Bae and Peter Csaba Ölveczky and Sharon Kim and Minseok Kang Modeling and formal analysis of virtually synchronous cyber-physical systems in AADL . . . . . . . . . . . . 911--948 Ramsay G. Taylor and Michael Foster and Siobhán North An automated framework for verifying or refuting trace properties of extended finite state machines . . . . . . . . . 949--972 Alberto Lluch Lafuente and Anastasia Mavridou Formal methods and tools for industrial critical systems . . . . . . . . . . . . 973--976 Cláudio Belo Lourenço and Denis Cousineau and Florian Faissole and Claude Marché and David Mentré and Hiroaki Inoue Automated formal analysis of temporal properties of Ladder programs . . . . . 977--997 Simon Thrane Hansen and Casper Thule and Cláudio Gomes and Jaco van de Pol and Maurizio Palmieri and Emin Oguz Inci and Frederik Madsen and Jesús Alfonso and José Ángel Castellanos and José Manuel Rodriguez Verification and synthesis of co-simulation algorithms subject to algebraic loops and adaptive steps . . . 999--1024 Andrej Kiviriga and Kim Guldstrand Larsen and Ulrik Nyman Randomized reachability analysis in UPPAAL: fast error detection in timed systems . . . . . . . . . . . . . . . . 1025--1042 Joshua Schmidt and Michael Leuschel SMT solving for the validation of B and Event-B models . . . . . . . . . . . . . 1043--1077
Alessandro Berti and Wil M. P. van der Aalst OC-PM: analyzing object-centric event logs and process models . . . . . . . . 1--17 Sascha Lehmann and Sibylle Schupp Bounded DBM-based clock state construction for timed automata in Uppaal . . . . . . . . . . . . . . . . . 19--47 Martina De Sanctis and Amleto Di Salle and Ludovico Iovino and Maria Teresa Rossi A technology transfer journey to a model-driven access control system . . . 49--74 Alfons Laarman and Ana Sokolova Introduction to the special issue for SPIN 2021 . . . . . . . . . . . . . . . 75--76 Alexandre Kirszenberg and Antoine Martin and Hugo Moreau and Etienne Renault Go2Pins: a framework for the LTL verification of Go programs (extended version) . . . . . . . . . . . . . . . . 77--94 Nicolas Amat and Silvano Dal Zilio and Didier Le Botlan Leveraging polyhedral reductions for solving Petri net reachability problems 95--114 Madoda Nxumalo and Nils Timm and Stefan Gruner An evaluation of approaches to model checking real-time task schedulability analysis . . . . . . . . . . . . . . . . 115--128
Peter Gjòl Jensen and Thomas Neele Tools and algorithms for the construction and analysis of systems: a special issue on tool papers for TACAS 2021 . . . . . . . . . . . . . . . . . . 129--131 Daniela Kaufmann and Armin Biere Improving AMulet2 for verifying multiplier circuits using SAT solving and computer algebra . . . . . . . . . . 133--144 Matthew Sotoudeh and Zhe Tao and Aditya V. Thakur SyReNN: a tool for analyzing deep neural networks . . . . . . . . . . . . . . . . 145--165 Yong Kiam Tan and Marijn J. H. Heule and Magnus O. Myreen Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML 167--184 Rosa Abbasi and Jonas Schiffl and Eva Darulova and Mattias Ulbrich and Wolfgang Ahrendt Combining rule- and SMT-based reasoning for verifying floating-point Java programs in KeY . . . . . . . . . . . . 185--204 Sebastian Biewer and Bernd Finkbeiner and Holger Hermanns and Maximilian A. Köhl and Yannik Schnitzer and Maximilian Schwenger On the road with RTLola . . . . . . . . 205--218 Joseph Scott and Aina Niemetz and Mathias Preiner and Saeed Nejati and Vijay Ganesh Algorithm selection for SMT . . . . . . 219--239
Nils Jansen and Gerrit Nolte and Bernhard Steffen Explanation Paradigms Leveraging Analytic Intuition (ExPLAIn) . . . . . . 241--247 Florian Jüngermann and Jan Kretínský and Maximilian Weininger Algebraically explainable controllers: decision trees and support vector machines join forces . . . . . . . . . . 249--266 Frederik Gossen and Bernhard Steffen Algebraic aggregation of random forests: towards explainability and rapid evaluation . . . . . . . . . . . . . . . 267--285 Alnis Murtovi and Alexander Bainczyk and Gerrit Nolte and Maximilian Schlüter and Bernhard Steffen Forest GUMP: a tool for verification and explanation . . . . . . . . . . . . . . 287--299 Maximilian Schlüter and Gerrit Nolte and Alnis Murtovi and Bernhard Steffen Towards rigorous understanding of neural networks via semantics-preserving transformations . . . . . . . . . . . . 301--327 Christopher Brix and Mark Niklas Müller and Stanley Bak and Taylor T. Johnson and Changliu Liu First three years of the international verification of neural networks competition (VNN-COMP) . . . . . . . . . 329--339 Igor Khmelnitsky and Daniel Neider and Rajarshi Roy and Xuan Xie and Beno\^\it Barbot and Benedikt Bollig and Alain Finkel and Serge Haddad and Martin Leucker and Lina Ye Analysis of recurrent neural networks via property-directed verification of surrogate models . . . . . . . . . . . . 341--354 Gerrit Nolte and Maximilian Schlüter and Alnis Murtovi and Bernhard Steffen The power of typed affine decision structures: a case study . . . . . . . . 355--374 Thom Badings and Thiago D. Simão and Marnix Suilen and Nils Jansen Decision-making under uncertainty: beyond probabilities . . . . . . . . . . 375--391 Muhammad Usman and Youcheng Sun and Divya Gopinath and Rishi Dange and Luca Manolache and Corina S. P\uas\uareanu An overview of structural coverage metrics for testing neural networks . . 393--405 Timo P. Gros and Holger Hermanns and Jörg Hoffmann and Michaela Klauck and Marcel Steinmetz Analyzing neural network behavior through deep statistical model checking 407--426
Jyotirmoy Deshmukh and Dejan Nickovi\'c Introduction to the Special Issue on Runtime Verification . . . . . . . . . . 427--429 Vivian M. Ho and Chris Alvin and Jimmie D. Lawson and Supratik Mukhopadhyay and Brian Peterson Program analysis using empirical abstraction . . . . . . . . . . . . . . 431--452 Chukri Soueidi and Marius Monnier and Yli\`es Falcone Efficient and expressive bytecode-level instrumentation for Java programs . . . 453--479 Nastaran Shafiei and Klaus Havelund and Peter Mehlitz Concurrent runtime verification of data rich events . . . . . . . . . . . . . . 481--501 Laura Nenzi and Ezio Bartocci and Luca Bortolussi and Simone Silvetti and Michele Loreti MoonLight: a lightweight tool for monitoring spatio-temporal properties 503--517 Lu Feng and Dana Fisman Introduction to the Special Issue on Runtime Verification . . . . . . . . . . 519--520 Vimuth Fernando and Keyur Joshi and Jacob Laurel and Sasa Misailovic Diamont: dynamic monitoring of uncertainty for distributed asynchronous programs . . . . . . . . . . . . . . . . 521--539 Anik Momtaz and Niraj Basnet and Houssam Abbas and Borzoo Bonakdarpour Predicate monitoring in distributed cyber-physical systems . . . . . . . . . 541--556 Konstantinos Mamouras and Agnishom Chattopadhyay and Zhifu Wang A compositional framework for algebraic quantitative online monitoring over continuous-time signals . . . . . . . . 557--573 Konstantin Kueffner and Anna Lukina and Christian Schilling and Thomas A. Henzinger Into the unknown: active monitoring of neural networks (extended version) . . . 575--592 Jan Baumeister and Johann C. Dauer and Bernd Finkbeiner and Sebastian Schirmer Monitoring with verified guarantees . . 593--616
Martin Wirsing and Stefan Jähnichen and Rocco De Nicola Rigorous engineering of collective adaptive systems --- 2nd special section 617--624 Marius Bozga and Joseph Sifakis Correct by design coordination of autonomous driving systems . . . . . . . 625--639 Davide Basile and Maurice H. ter Beek and Laura Bussi and Vincenzo Ciancia A toolchain for strategy synthesis with spatial properties . . . . . . . . . . . 641--658 Peter Fettke and Wolfgang Reisig A causal, time-independent synchronization pattern for collective adaptive systems . . . . . . . . . . . . 659--673 Rocco De Nicola and Luca Di Stefano and Omar Inverso and Serenella Valiani Modelling flocks of birds and colonies of ants from the bottom up . . . . . . . 675--691 Stefania Monica and Federico Bergenti and Franco Zambonelli A kinetic approach to investigate the collective dynamics of multi-agent systems . . . . . . . . . . . . . . . . 693--705 Chen Yifeng and J. W. Sanders A modal approach to conscious social agents . . . . . . . . . . . . . . . . . 707--716 Michal Töpfer and Milad Abdullah and Tomá\vs Bure\vs and Petr Hn\vetynka and Martin Kruli\vs Machine-learning abstractions for component-based self-optimizing systems 717--731 Tomá\vs Bure\vs and Petr Hn\vetynka and Martin Kruli\vs and Franti\vsek Plá\vsil and Danylo Khalyeyev and Sebastian Hahner and Stephan Seifermann and Maximilian Walter and Robert Heinrich Generating adaptation rule-specific neural networks . . . . . . . . . . . . 733--746 Lorenzo Bettini and Khalid Bourr and Rosario Pugliese and Francesco Tiezzi Coordinating and programming multiple ROS-based robots with X-KLAIM . . . . . 747--764 Yehia Abd Alrahman and Shaun Azzopardi and Luca Di Stefano and Nir Piterman Language support for verifying reconfigurable interacting systems . . . 765--784 Maurizio Murgia and Riccardo Pinciroli and Catia Trubiani and Emilio Tuosto Comparing performance abstractions for collective adaptive systems . . . . . . 785--798 Joseph Scott and Aina Niemetz and Mathias Preiner and Saeed Nejati and Vijay Ganesh Publisher Correction: Algorithm selection for SMT . . . . . . . . . . . 799--800
Guisella Angulo and Daniel San Martín and Fabiano Ferrari and Ignacio García-Rodríguez de Guzmán and Ricardo Perez-Castillo and Valter Vieira de Camargo A process for creating KDM2PSM transformation engines . . . . . . . . . 1--20 Joanna Kosi\'nska and Grzegorz Broto\'n and Maciej Tobiasz Knowledge representation of the state of a cloud-native application . . . . . . . 21--32 Klaus Havelund and Gerard J. Holzmann Programming event monitors . . . . . . . 33--47 Stefan Schupp and Erika Ábrahám and Md Tawhid Bin Waez and Thomas Rambow and Zeng Qiu On the applicability of hybrid systems safety verification tools from the automotive perspective . . . . . . . . . 49--78 Tomoya Yamaguchi and Bardh Hoxha and Dejan Nickovi\'c RTAMT --- Runtime Robustness Monitors with Application to CPS and Robotics . . 79--99 Martijn Hendriks and Jacques Verriet and Twan Basten Visualization, transformation, and analysis of execution traces with the eclipse TRACE4CPS trace tool . . . . . . 101--126
Jan Friso Groote and Marieke Huisman Formal Methods for Industrial Critical Systems . . . . . . . . . . . . . . . . 127--129 Franck Cassez and Joanne Fuller and Horacio Mijail Antón Quiles Deductive verification of smart contracts with Dafny . . . . . . . . . . 131--145 Fabian Vu and Christopher Happe and Michael Leuschel Generating interactive documents for domain-specific validation of formal models . . . . . . . . . . . . . . . . . 147--168 André Matos Pedro and Tomás Silva and Tiago Sequeira and João Lourenço and João Costa Seco and Carla Ferreira Monitoring of spatio-temporal properties with nonlinear SAT solvers . . . . . . . 169--188 Mélanie Ducoffe and Christophe Gabreau and Ileana Ober and Iulian Ober and Eric Guillaume Vidot Certification of avionic software based on machine learning: the case for formal monotony analysis . . . . . . . . . . . 189--205 Anton Hampus and Mattias Nyberg Formally verifying decompositions of stochastic specifications . . . . . . . 207--228 Julius Adelt and Julian Gebker and Paula Herber Reusable formal models for concurrency and communication in custom real-time operating systems . . . . . . . . . . . 229--245
Bernhard Steffen Rance Cleaveland: a life for formal methods . . . . . . . . . . . . . . . . 247--248 Zixin Huang and Saikat Dutta and Sasa Misailovic Debugging convergence problems in probabilistic programs via program representation learning with SixthSense 249--268 Leonore Winterer and Ralf Wimmer and Bernd Becker and Nils Jansen Strong Simple Policies for POMDPs . . . 269--299 Manuel Leithner and Andrea Bombarda and Michael Wagner and Angelo Gargantini and Dimitris E. Simos State of the CArt: evaluating covering array generators at scale . . . . . . . 301--326 Alexander Raschke and Dominique Méry An automotive case study . . . . . . . . 327--330 Amel Mammar and Marc Frappier and Régine Laleau An Event-B model of an automotive adaptive exterior light system . . . . . 331--346 Amel Mammar and Marc Frappier Modeling of a speed control system using Event-B . . . . . . . . . . . . . . . . 347--363 Alcino Cunha and Nuno Macedo and Chong Liu Validating multiple variants of an automotive light system with Alloy 6 . . 365--377 Paolo Arcaini and Silvia Bonfanti and Angelo Gargantini and Elvinia Riccobene and Patrizia Scandurra A journey with ASMETA from requirements to code: application to an automotive system with adaptive features . . . . . 379--401 Sebastian Krings and Philipp Körner and Jannik Dunkelau and Kristin Rutenkolk A verified low-level implementation and visualization of the adaptive exterior light and speed control system . . . . . 403--419