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

Last update: Sun Feb 18 14:57:54 MST 2018                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


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
          Francois 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 KeYmaera: 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