Table of contents for issues of International Journal on Software Tools for Technology Transfer (STTT)

Last update: Thu Aug 29 06:18:57 MDT 2024                Valid HTML 3.2!

Volume 1, Number 1--2, December, 1997
Volume 2, Number 1, November, 1998
Volume 2, Number 2, December, 1998
Volume 2, Number 3, November, 1999
Volume 2, Number 4, March, 2000
Volume 3, Number 1, September, 2000
Volume 3, Number 2, May, 2001
Volume 3, Number 3, August, 2001
Volume 3, Number 4, September, 2001
Volume 4, Number 1, October, 2002
Volume 4, Number 2, February, 2003
Volume 4, Number 3, May, 2003
Volume 4, Number 4, August, 2003
Volume 5, Number 1, November, 2003
Volume 5, Number 2--3, March, 2004
Volume 5, Number 4, May, 2004
Volume 6, Number 1, July, 2004
Volume 6, Number 2, August, 2004
Volume 6, Number 3, August, 2004
Volume 6, Number 4, August, 2004
Volume 7, Number 1, February, 2005
Volume 7, Number 2, April, 2005
Volume 7, Number 3, June, 2005
Volume 7, Number 4, August, 2005
Volume 8, Number 1, February, 2006
Volume 8, Number 2, April, 2006
Volume 8, Number 3, June, 2006
Volume 8, Number 4--5, August, 2006
Volume 8, Number 6, November, 2006
Volume 9, Number 1, February, 2007
Volume 9, Number 2, March, 2007
Volume 9, Number 3--4, June, 2007
Volume 9, Number 5--6, October, 2007
Volume 10, Number 1, January, 2008
Volume 10, Number 2, March, 2008
Volume 10, Number 3, June, 2008
Volume 10, Number 4, August, 2008
Volume 10, Number 5, October, 2008
Volume 10, Number 6, December, 2008
Volume 11, Number 1, February, 2009
Volume 11, Number 2, April, 2009
Volume 11, Number 3, July, 2009
Volume 11, Number 4, October, 2009
Volume 11, Number 5, November, 2009
Volume 11, Number 6, December, 2009
Volume 12, Number 1, February, 2010
Volume 12, Number 2, May, 2010
Volume 12, Number 3--4, July, 2010
Volume 12, Number 5, September, 2010
Volume 12, Number 6, November, 2010
Volume 13, Number 1, January, 2011
Volume 13, Number 2, April, 2011
Volume 13, Number 3, June, 2011
Volume 13, Number 4, August, 2011
Volume 13, Number 5, October, 2011
Volume 13, Number 6, November, 2011
Volume 14, Number 1, February, 2012
Volume 14, Number 2, April, 2012
Volume 14, Number 3, June, 2012
Volume 14, Number 4, August, 2012
Volume 14, Number 5, October, 2012
Volume 14, Number 6, November, 2012
Volume 15, Number 1, February, 2013
Volume 15, Number 2, April, 2013
Volume 15, Number 3, June, 2013
Volume 15, Number 4, August, 2013
Volume 15, Number 5--6, October, 2013
Volume 16, Number 1, February, 2014
Volume 16, Number 2, April, 2014
Volume 16, Number 3, June, 2014
Volume 16, Number 4, August, 2014
Volume 16, Number 5, October, 2014
Volume 16, Number 6, November, 2014
Volume 17, Number 1, February, 2015
Volume 17, Number 2, April, 2015
Volume 17, Number 3, June, 2015
Volume 17, Number 4, August, 2015
Volume 17, Number 5, October, 2015
Volume 17, Number 6, November, 2015
Volume 18, Number 1, February, 2016
Volume 18, Number 2, April, 2016
Volume 18, Number 3, June, 2016
Volume 18, Number 4, August, 2016
Volume 18, Number 5, October, 2016
Volume 18, Number 6, November, 2016
Volume 19, Number 1, February, 2017
Volume 19, Number 2, April, 2017
Volume 19, Number 3, June, 2017
Volume 19, Number 4, August, 2017
Volume 19, Number 5, October, 2017
Volume 19, Number 6, November, 2017
Volume 20, Number 1, February, 2018
Volume 20, Number 2, April, 2018
Volume 20, Number 3, June, 2018
Volume 20, Number 4, August, 2018
Volume 20, Number 5, October, 2018
Volume 20, Number 6, November, 2018
Volume 21, Number 1, February, 2019
Volume 21, Number 2, April, 2019
Volume 21, Number 3, June, 2019
Volume 21, Number 4, August, 2019
Volume 21, Number 5, October, 2019
Volume 21, Number 6, December, 2019
Volume 22, Number 1, February, 2020
Volume 22, Number 2, April, 2020
Volume 22, Number 3, June, 2020
Volume 22, Number 4, August, 2020
Volume 22, Number 5, October, 2020
Volume 22, Number 6, December, 2020
Volume 23, Number 1, February, 2021
Volume 23, Number 2, April, 2021
Volume 23, Number 3, June, 2021
Volume 23, Number 4, August, 2021
Volume 23, Number 5, October, 2021
Volume 23, Number 6, December, 2021
Volume 24, Number 1, February, 2022
Volume 24, Number 2, April, 2022
Volume 24, Number 3, June, 2022
Volume 24, Number 4, August, 2022
Volume 24, Number 5, October, 2022
Volume 24, Number 6, December, 2022
Volume 25, Number 1, February, 2023
Volume 25, Number 2, April, 2023
Volume 25, Number 3, June, 2023
Volume 25, Number 4, August, 2023
Volume 25, Number 5--6, December, 2023
Volume 26, Number 1, February, 2024
Volume 26, Number 2, April, 2024
Volume 26, Number 3, June, 2024


International Journal on Software Tools for Technology Transfer (STTT)
Volume 1, Number 1--2, December, 1997

        W. 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


International Journal on Software Tools for Technology Transfer (STTT)
Volume 2, Number 1, November, 1998

                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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 2, Number 2, December, 1998

                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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 2, Number 3, November, 1999

              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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 2, Number 4, March, 2000

          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


International Journal on Software Tools for Technology Transfer (STTT)
Volume 3, Number 1, September, 2000

         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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 3, Number 2, May, 2001

                    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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 3, Number 3, August, 2001

               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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 3, Number 4, September, 2001

                    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


International Journal on Software Tools for Technology Transfer (STTT)
Volume 4, Number 1, October, 2002

                      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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 4, Number 2, February, 2003

                   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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 4, Number 3, May, 2003

              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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 4, Number 4, August, 2003

                 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


International Journal on Software Tools for Technology Transfer (STTT)
Volume 5, Number 1, November, 2003

           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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 5, Number 2--3, March, 2004

                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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 5, Number 4, May, 2004

      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


International Journal on Software Tools for Technology Transfer (STTT)
Volume 6, Number 1, July, 2004

                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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 6, Number 2, August, 2004

        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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 6, Number 3, August, 2004

            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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 6, Number 4, August, 2004

              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


International Journal on Software Tools for Technology Transfer (STTT)
Volume 7, Number 1, February, 2005

               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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 7, Number 2, April, 2005

                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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 7, Number 3, June, 2005

                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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 7, Number 4, August, 2005

               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


International Journal on Software Tools for Technology Transfer (STTT)
Volume 8, Number 1, February, 2006

             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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 8, Number 2, April, 2006

               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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 8, Number 3, June, 2006

                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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 8, Number 4--5, August, 2006

         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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 8, Number 6, November, 2006

           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


International Journal on Software Tools for Technology Transfer (STTT)
Volume 9, Number 1, February, 2007

             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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 9, Number 2, March, 2007

         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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 9, Number 3--4, June, 2007

                    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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 9, Number 5--6, October, 2007

         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


International Journal on Software Tools for Technology Transfer (STTT)
Volume 10, Number 1, January, 2008

                    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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 10, Number 2, March, 2008

            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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 10, Number 3, June, 2008

       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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 10, Number 4, August, 2008

         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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 10, Number 5, October, 2008

    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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 10, Number 6, December, 2008

           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


International Journal on Software Tools for Technology Transfer (STTT)
Volume 11, Number 1, February, 2009

                  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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 11, Number 2, April, 2009

               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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 11, Number 3, July, 2009

               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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 11, Number 4, October, 2009

                    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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 11, Number 5, November, 2009

           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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 11, Number 6, December, 2009

              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


International Journal on Software Tools for Technology Transfer (STTT)
Volume 12, Number 1, February, 2010

           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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 12, Number 2, May, 2010

            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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 12, Number 3--4, July, 2010

              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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 12, Number 5, September, 2010

             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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 12, Number 6, November, 2010

            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


International Journal on Software Tools for Technology Transfer (STTT)
Volume 13, Number 1, January, 2011

            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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 13, Number 2, April, 2011

                   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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 13, Number 3, June, 2011

              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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 13, Number 4, August, 2011

              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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 13, Number 5, October, 2011

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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 13, Number 6, November, 2011

              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


International Journal on Software Tools for Technology Transfer (STTT)
Volume 14, Number 1, February, 2012

          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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 14, Number 2, April, 2012

            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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 14, Number 3, June, 2012

              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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 14, Number 4, August, 2012

         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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 14, Number 5, October, 2012

               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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 14, Number 6, November, 2012

                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


International Journal on Software Tools for Technology Transfer (STTT)
Volume 15, Number 1, February, 2013

              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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 15, Number 2, April, 2013

        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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 15, Number 3, June, 2013

            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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 15, Number 4, August, 2013

          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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 15, Number 5--6, October, 2013

            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


International Journal on Software Tools for Technology Transfer (STTT)
Volume 16, Number 1, February, 2014

            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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 16, Number 2, April, 2014

            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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 16, Number 3, June, 2014

             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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 16, Number 4, August, 2014

           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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 16, Number 5, October, 2014

                 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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 16, Number 6, November, 2014

        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


International Journal on Software Tools for Technology Transfer (STTT)
Volume 17, Number 1, February, 2015

             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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 17, Number 2, April, 2015

            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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 17, Number 3, June, 2015

           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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 17, Number 4, August, 2015

                 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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 17, Number 5, October, 2015

             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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 17, Number 6, November, 2015

            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


International Journal on Software Tools for Technology Transfer (STTT)
Volume 18, Number 1, February, 2016

         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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 18, Number 2, April, 2016

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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 18, Number 3, June, 2016

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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 18, Number 4, August, 2016

              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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 18, Number 5, October, 2016

          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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 18, Number 6, November, 2016

        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


International Journal on Software Tools for Technology Transfer (STTT)
Volume 19, Number 1, February, 2017

               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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 19, Number 2, April, 2017

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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 19, Number 3, June, 2017

            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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 19, Number 4, August, 2017

     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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 19, Number 5, October, 2017

                   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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 19, Number 6, November, 2017

             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


International Journal on Software Tools for Technology Transfer (STTT)
Volume 20, Number 1, February, 2018

              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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 20, Number 2, April, 2018

                  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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 20, Number 3, June, 2018

        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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 20, Number 4, August, 2018

        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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 20, Number 5, October, 2018

            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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 20, Number 6, November, 2018

            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


International Journal on Software Tools for Technology Transfer (STTT)
Volume 21, Number 1, February, 2019

                 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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 21, Number 2, April, 2019

            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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 21, Number 3, June, 2019

             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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 21, Number 4, August, 2019

       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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 21, Number 5, October, 2019

           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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 21, Number 6, December, 2019

        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


International Journal on Software Tools for Technology Transfer (STTT)
Volume 22, Number 1, February, 2020

           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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 22, Number 2, April, 2020

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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 22, Number 3, June, 2020

             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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 22, Number 4, August, 2020

                 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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 22, Number 5, October, 2020

                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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 22, Number 6, December, 2020

                      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


International Journal on Software Tools for Technology Transfer (STTT)
Volume 23, Number 1, February, 2021

       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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 23, Number 2, April, 2021

             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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 23, Number 3, June, 2021

         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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 23, Number 4, August, 2021

              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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 23, Number 5, October, 2021

             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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 23, Number 6, December, 2021

                 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


International Journal on Software Tools for Technology Transfer (STTT)
Volume 24, Number 1, February, 2022

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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 24, Number 2, April, 2022

         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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 24, Number 3, June, 2022

        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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 24, Number 4, August, 2022

               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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 24, Number 5, October, 2022

                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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 24, Number 6, December, 2022

          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


International Journal on Software Tools for Technology Transfer (STTT)
Volume 25, Number 1, February, 2023

           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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 25, Number 2, April, 2023

   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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 25, Number 3, June, 2023

                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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 25, Number 4, August, 2023

         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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 25, Number 5--6, December, 2023

             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


International Journal on Software Tools for Technology Transfer (STTT)
Volume 26, Number 1, February, 2024

            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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 26, Number 2, April, 2024

           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

International Journal on Software Tools for Technology Transfer (STTT)
Volume 26, Number 3, June, 2024

               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