| no |
title |
author |
magazine |
year |
volume |
issue |
page(s) |
type |
| 1 |
Abstraction and approximation in fuzzy temporal logics and models
|
Sotudeh, Gholamreza
|
|
2014
|
|
2 |
p. 309-334
|
article
|
| 2 |
A Case Study in the Specification and Analysis of Design Alternatives for a User Interface
|
Duke, David
|
|
1999
|
|
2 |
p. 107-131
|
article
|
| 3 |
Action Refinement Applied to Late Decisions
|
Fecher, H.
|
|
2006
|
|
2 |
p. 211-230
|
article
|
| 4 |
Active learning for extended finite state machines
|
Cassel, Sofia
|
|
2016
|
|
2 |
p. 233-263
|
article
|
| 5 |
Adaptive distinguishing test cases of nondeterministic finite state machines: test case derivation and length estimation
|
El-Fakih, Khaled
|
|
2018
|
|
2 |
p. 319-332
|
article
|
| 6 |
A denotational semantics for Handel-C
|
Butterfield, Andrew
|
|
2009
|
|
2 |
p. 153-170
|
article
|
| 7 |
ADL: An Activity Description Language for Real-Time Networks
|
Paynter, Stephen
|
|
2000
|
|
2 |
p. 120-144
|
article
|
| 8 |
A formal approach for the construction and verification of railway control systems
|
Haxthausen, Anne E.
|
|
2009
|
|
2 |
p. 191-219
|
article
|
| 9 |
A formal approach to adaptive software: continuous assurance of non-functional requirements
|
Filieri, Antonio
|
|
2011
|
|
2 |
p. 163-186
|
article
|
| 10 |
A formalization of geometric constraint systems and their decomposition
|
Mathis, Pascal
|
|
2009
|
|
2 |
p. 129-151
|
article
|
| 11 |
A formal relationship between program slicing and partial evaluation
|
Binkley, David W.
|
|
2006
|
|
2 |
p. 103-119
|
article
|
| 12 |
A general framework for architecture composability
|
Attie, Paul
|
|
2015
|
|
2 |
p. 207-231
|
article
|
| 13 |
Algebra and logic for access control
|
Collinson, Matthew
|
|
2009
|
|
2 |
p. 83-104
|
article
|
| 14 |
A linear algebra approach to OLAP
|
Macedo, Hugo Daniel
|
|
2014
|
|
2 |
p. 283-307
|
article
|
| 15 |
A Maude environment for CafeOBJ
|
Riesco, Adrián
|
|
2016
|
|
2 |
p. 309-334
|
article
|
| 16 |
A mini challenge: build a verifiable filesystem
|
Joshi, Rajeev
|
|
2007
|
|
2 |
p. 269-272
|
article
|
| 17 |
Amílcar Sernadas
|
|
|
2017
|
|
2 |
p. 173
|
article
|
| 18 |
Analysing Cognitive Behaviour using LOTOS and Mexitl
|
Bowman, Howard
|
|
1999
|
|
2 |
p. 132-159
|
article
|
| 19 |
An empirical comparison of formalisms for modelling and analysis of dynamic reconfiguration of dependable systems
|
Bhattacharyya, Anirban
|
|
2017
|
|
2 |
p. 251-307
|
article
|
| 20 |
An explicit transition system construction approach to LTL satisfiability checking
|
Li, Jianwen
|
|
2017
|
|
2 |
p. 193-217
|
article
|
| 21 |
An inductive characterization of matching in binding bigraphs
|
Damgaard, Troels C.
|
|
2011
|
|
2 |
p. 257-288
|
article
|
| 22 |
An Introduction to Real-Time Object-Z
|
Smith, Graeme
|
|
2002
|
|
2 |
p. 128-141
|
article
|
| 23 |
A Note on Kobayashi's and Yonezawa's “Asynchronous Communication Model Based on Linear Logic”
|
de Groote, Philippe
|
|
1998
|
|
2 |
p. 160-170
|
article
|
| 24 |
An Overview of the Integrated Formalism RT-Z
|
Sühl, Carsten
|
|
2002
|
|
2 |
p. 94-110
|
article
|
| 25 |
A practical comparison of Alloy and Spin
|
Zave, P.
|
|
2014
|
|
2 |
p. 239-253
|
article
|
| 26 |
A process algebraic framework for specification and validation of real-time systems
|
Sherif, Adnan
|
|
2009
|
|
2 |
p. 153-191
|
article
|
| 27 |
A process calculus BigrTiMo of mobile systemsand its formal semantics
|
Xie, Wanling
|
|
|
|
2 |
p. 207-249
|
article
|
| 28 |
A Program Refinement Tool
|
Carrington, D.
|
|
BCS
|
|
2 |
p. 97-124
|
article
|
| 29 |
A Program Refinement Tool
|
Carrington, D.
|
|
|
|
2 |
p. 97-124
|
article
|
| 30 |
A refinement-based process algebra for timed automata
|
Cattani, Stefano
|
|
2005
|
|
2 |
p. 138-159
|
article
|
| 31 |
A Refinement Calculus for Shared-Variable Parallel and Distributed Programming
|
Dingel, J.
|
|
2002
|
|
2 |
p. 123-197
|
article
|
| 32 |
Are the Logical Foundations of Verifying Compiler Prototypes Matching user Expectations?
|
Chalin, Patrice
|
|
2007
|
|
2 |
p. 139-158
|
article
|
| 33 |
A singleton failures semantics for Communicating Sequential Processes
|
Bolton, Christie
|
|
2006
|
|
2 |
p. 181-210
|
article
|
| 34 |
Assertion-based slicing and slice graphs
|
Barros, José Bernardo
|
|
2011
|
|
2 |
p. 217-248
|
article
|
| 35 |
A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
|
Hayes, Ian J.
|
|
2018
|
|
2 |
p. 133-163
|
article
|
| 36 |
Automated mutual induction proof in separation logic
|
Ta, Quang-Trung
|
|
2018
|
|
2 |
p. 207-230
|
article
|
| 37 |
Battery-aware scheduling in low orbit: the GomX–3 case
|
Bisgaard, Morten
|
|
2018
|
|
2 |
p. 261-285
|
article
|
| 38 |
Building program construction and verification tools from algebraic principles
|
Armstrong, Alasdair
|
|
2015
|
|
2 |
p. 265-293
|
article
|
| 39 |
Code-carrying theories
|
Jacobs, Bart
|
|
2006
|
|
2 |
p. 191-203
|
article
|
| 40 |
Combining Component Specifications in Object-Z and CSP
|
Derrick, John
|
|
2002
|
|
2 |
p. 111-127
|
article
|
| 41 |
Comparing model checking and logical reasoning for real-time systems
|
Dierks, Henning
|
|
2004
|
|
2 |
p. 104-120
|
article
|
| 42 |
Complete model-based equivalence class testing for nondeterministic systems
|
Huang, Wen-ling
|
|
2016
|
|
2 |
p. 335-364
|
article
|
| 43 |
Completeness of a combination of neighbourhood logic and temporal logic
|
Barua, Rana
|
|
2004
|
|
2 |
p. 96-103
|
article
|
| 44 |
Compositional Comparison of Formal Software Specifications Using Transformation Systems
|
Große-Rhode, Martin
|
|
2002
|
|
2 |
p. 161-186
|
article
|
| 45 |
Construction and analysis of ground models and their refinements as a foundation for validating computer-based systems
|
Börger, Egon
|
|
2007
|
|
2 |
p. 225-241
|
article
|
| 46 |
Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application
|
Banach, Richard
|
|
2012
|
|
2 |
p. 319-366
|
article
|
| 47 |
Correctness and concurrent complexity of the Black-White Bakery Algorithm
|
Hesselink, Wim H.
|
|
2016
|
|
2 |
p. 325-341
|
article
|
| 48 |
Cut Set Analysis using Behavior Trees and model checking
|
Lindsay, Peter A.
|
|
2011
|
|
2 |
p. 249-266
|
article
|
| 49 |
Deep Semantic Links of TCSP and Object-Z: TCOZ Approach
|
Mahony, Brendan
|
|
2002
|
|
2 |
p. 142-160
|
article
|
| 50 |
Derivation of concurrent programs by stepwise scheduling of Event-B models
|
Boström, Pontus
|
|
2012
|
|
2 |
p. 281-303
|
article
|
| 51 |
Deriving bisimulation relations from path based equivalence checkers
|
Banerjee, Kunal
|
|
2016
|
|
2 |
p. 365-379
|
article
|
| 52 |
Discovery of invariants through automated theory formation
|
Llano, Maria Teresa
|
|
2012
|
|
2 |
p. 203-249
|
article
|
| 53 |
Duration-constrained regular expressions
|
Xuandong, Li
|
|
2004
|
|
2 |
p. 155-163
|
article
|
| 54 |
Editorial
|
JONES, CLIFF
|
|
2002
|
|
2 |
p. 91
|
article
|
| 55 |
Editorial
|
Liu, Zhiming
|
|
2011
|
|
2 |
p. 151
|
article
|
| 56 |
Editorial
|
Boiten, Eerke A.
|
|
2014
|
|
2 |
p. 195
|
article
|
| 57 |
Editorial
|
Jones, Cliff
|
|
2004
|
|
2 |
p. 95
|
article
|
| 58 |
Editorial
|
Fiadeiro, J. L.
|
|
2012
|
|
2 |
p. 161-162
|
article
|
| 59 |
Editorial
|
Giannakopoulou, Dimitra
|
|
2016
|
|
2 |
p. 179-180
|
article
|
| 60 |
Editorial
|
Gnesi, Stefania
|
|
2019
|
|
2 |
p. 131-132
|
article
|
| 61 |
Editorial
|
Cooke, John
|
|
2002
|
|
2 |
p. 93
|
article
|
| 62 |
Editorial (VSTTE Special Issue)
|
Cooke, J.
|
|
2007
|
|
2 |
p. 137-138
|
article
|
| 63 |
Edsger Wybe Dijkstra (1930–2002): A Portrait of a Genius
|
Apt, Krzysztof R.
|
|
2002
|
|
2 |
p. 92-98
|
article
|
| 64 |
Edsger Wybe Dijkstra (1930–2002): A Portrait of a Genius
|
Apt, Krzysztof R.
|
|
|
|
2 |
p. 92-98
|
article
|
| 65 |
EWD1300: The Notational Conventions I Adopted, and Why
|
Dijkstra, Edsger W.
|
|
2002
|
|
2 |
p. 99-107
|
article
|
| 66 |
Expressive Power of Specification Languages
|
Hayes, Ian J.
|
|
1998
|
|
2 |
p. 187-192
|
article
|
| 67 |
Finding suitable variability abstractions for lifted analysis
|
Dimovski, Aleksandar S.
|
|
2019
|
|
2 |
p. 231-259
|
article
|
| 68 |
Finite Integer Computations: An Algebraic Foundation for Their Correctness
|
Glesner, Sabine
|
|
2006
|
|
2 |
p. 244-262
|
article
|
| 69 |
Formal Aspects of Correctness and Optimality of Interval Computations
|
Santiago, Regivan H. Nunes
|
|
2006
|
|
2 |
p. 231-243
|
article
|
| 70 |
Formalising a Value-Passing Calculus in HOL
|
Nesi, Monica
|
|
1999
|
|
2 |
p. 160-199
|
article
|
| 71 |
Formalizing and testing the consistency of DSL transformations
|
Keshishzadeh, Sarmen
|
|
2016
|
|
2 |
p. 181-206
|
article
|
| 72 |
Formalizing provable anonymity in Isabelle/HOL
|
Li, Yongjian
|
|
2014
|
|
2 |
p. 255-282
|
article
|
| 73 |
Formally sound implementations of security protocols with JavaSPI
|
Sisto, Riccardo
|
|
2017
|
|
2 |
p. 279-317
|
article
|
| 74 |
Formal verification and quantitative metrics of MPSoC data dynamics
|
Zhang, Hui
|
|
2017
|
|
2 |
p. 219-237
|
article
|
| 75 |
Generalised folds for nested datatypes
|
Bird, Richard
|
|
1999
|
|
2 |
p. 200-222
|
article
|
| 76 |
Generating certified code from formal proofs: a case study in homological algebra
|
Aransay, Jesús
|
|
2009
|
|
2 |
p. 193-213
|
article
|
| 77 |
Generic Composition
|
Chen, Yifeng
|
|
2002
|
|
2 |
p. 108-122
|
article
|
| 78 |
Guest Editorial
|
Leuschel, Michael
|
|
2005
|
|
2 |
p. 91-92
|
article
|
| 79 |
Highly dependable concurrent programming using design for verification
|
Betin-Can, Aysu
|
|
2006
|
|
2 |
p. 243-268
|
article
|
| 80 |
Hybrid statistical estimation of mutual information and its application to information flow
|
Biondi, Fabrizio
|
|
2018
|
|
2 |
p. 165-206
|
article
|
| 81 |
Improved algorithms for optimal length resolution refutation in difference constraint systems
|
Subramani, K.
|
|
2011
|
|
2 |
p. 319-341
|
article
|
| 82 |
In memoriam: Professor Heinz Zemanek (1920–2014)
|
Jones, Cliff B.
|
|
2015
|
|
2 |
p. 237
|
article
|
| 83 |
Integrating a formal method into a software engineering process with UML and Java
|
Möller, Michael
|
|
2007
|
|
2 |
p. 161-204
|
article
|
| 84 |
Interface synthesis and protocol conversion
|
Bhaduri, Purandar
|
|
2007
|
|
2 |
p. 205-224
|
article
|
| 85 |
Interval timed coloured Petri net: efficient construction of its state class space preserving linear properties
|
Boucheneb, Hanifa
|
|
2007
|
|
2 |
p. 225-238
|
article
|
| 86 |
Introducing extra operations in refinement
|
Boiten, Eerke A.
|
|
2012
|
|
2 |
p. 305-317
|
article
|
| 87 |
Kaisa Sere: In Memoriam
|
Petre, Luigia
|
|
2013
|
|
2 |
p. 197-201
|
article
|
| 88 |
Laws of mission-based programming
|
Zeyda, Frank
|
|
2014
|
|
2 |
p. 423-472
|
article
|
| 89 |
Manifest domains: analysis and description
|
Bjørner, Dines
|
|
2016
|
|
2 |
p. 175-225
|
article
|
| 90 |
Maximally Concurrent Programs
|
Joshi, Rajeev
|
|
2000
|
|
2 |
p. 100-119
|
article
|
| 91 |
Minimal refinements of specifications in modal and temporal logics
|
Gorogiannis, Nikos
|
|
2007
|
|
2 |
p. 273
|
article
|
| 92 |
Model-based Safety Assessment of a Triple Modular Generator with xSAP
|
Bozzano, Marco
|
|
|
|
2 |
p. 251-295
|
article
|
| 93 |
Model-checking dense-time Duration Calculus
|
Fränzle, Martin
|
|
2004
|
|
2 |
p. 121-139
|
article
|
| 94 |
Model checking dynamic pushdown networks
|
Song, Fu
|
|
2015
|
|
2 |
p. 397-421
|
article
|
| 95 |
Model checking, testing and verification working together
|
Gunter, Elsa
|
|
2005
|
|
2 |
p. 201-221
|
article
|
| 96 |
Model-checking timed automata with deadlines with Uppaal
|
Gómez, Rodolfo
|
|
2011
|
|
2 |
p. 289-318
|
article
|
| 97 |
Modeling and analysis of communicating systems
|
Rossi, Matteo
|
|
|
|
2 |
p. 297-298
|
article
|
| 98 |
Natural Semantics-Directed Generation of Compilers and Abstract Machines
|
Diehl, Stephan
|
|
2000
|
|
2 |
p. 71-99
|
article
|
| 99 |
Not necessarily closed convex polyhedra and the double description method
|
Bagnara, Roberto
|
|
2005
|
|
2 |
p. 222-257
|
article
|
| 100 |
On assertion-based encapsulation for object invariants and simulations
|
Naumann, David A.
|
|
2006
|
|
2 |
p. 205-224
|
article
|
| 101 |
On the expressive power of CSP refinement
|
Roscoe, A.W.
|
|
2005
|
|
2 |
p. 93-112
|
article
|
| 102 |
On the Interactive Power of Higher-order Processes Extended with Parameterization
|
Zhang, Wenbo
|
|
|
|
2 |
p. 151-183
|
article
|
| 103 |
On the limits of refinement-testing for model-checking CSP
|
Murray, Toby
|
|
2011
|
|
2 |
p. 219-256
|
article
|
| 104 |
Optimising the ProB model checker for B using partial order reduction
|
Dobrikov, Ivaylo
|
|
2016
|
|
2 |
p. 295-323
|
article
|
| 105 |
Procedure compilation in the refinement calculus
|
Lermer, K.
|
|
2006
|
|
2 |
p. 152-180
|
article
|
| 106 |
Proof-based verification approaches for dynamic properties: application to the information system domain
|
Mammar, Amel
|
|
2014
|
|
2 |
p. 335-374
|
article
|
| 107 |
Provably-correct hardware compilation tools based on pass separation techniques
|
McKeever, Steve
|
|
2005
|
|
2 |
p. 120-142
|
article
|
| 108 |
Refinement-based verification of implementations of Stateflow charts
|
Miyazawa, Alvaro
|
|
2013
|
|
2 |
p. 367-405
|
article
|
| 109 |
Refinement in hybridised institutions
|
Madeira, Alexandre
|
|
2014
|
|
2 |
p. 375-395
|
article
|
| 110 |
Refinement is complete for implementations
|
Huth, Michael
|
|
2005
|
|
2 |
p. 113-137
|
article
|
| 111 |
Refining autonomous agents with declarative beliefs and desires
|
Li, Qin
|
|
2016
|
|
2 |
p. 227-249
|
article
|
| 112 |
Relating computer systems to sequence diagrams: the impact of underspecification and inherent nondeterminism
|
Runde, Ragnhild Kobro
|
|
2011
|
|
2 |
p. 159-187
|
article
|
| 113 |
Relational concurrent refinement part III: traces, partial relations and automata
|
Derrick, John
|
|
2012
|
|
2 |
p. 407-432
|
article
|
| 114 |
Reo + mCRL2 : A framework for model-checking dataflow in service compositions
|
Kokash, Natallia
|
|
2011
|
|
2 |
p. 187-216
|
article
|
| 115 |
Scalable context-dependent analysis of emergency egress models
|
Massink, M.
|
|
2011
|
|
2 |
p. 267-302
|
article
|
| 116 |
Specification and verification challenges for sequential object-oriented programs
|
Leavens, Gary T.
|
|
2007
|
|
2 |
p. 159-189
|
article
|
| 117 |
Specifying and Refining Internal Operations in Z
|
Derrick, John
|
|
1998
|
|
2 |
p. 125-159
|
article
|
| 118 |
Streamlining progress-based derivations of concurrent programs
|
Dongol, Brijesh
|
|
2007
|
|
2 |
p. 141-160
|
article
|
| 119 |
Symbolic decision procedure for termination of linear programs
|
Xia, Bican
|
|
2009
|
|
2 |
p. 171-190
|
article
|
| 120 |
The behavioural semantics of Event-B refinement
|
Schneider, Steve
|
|
2012
|
|
2 |
p. 251-280
|
article
|
| 121 |
The data type of spatial objects
|
Johnson, Kenneth
|
|
2011
|
|
2 |
p. 189-218
|
article
|
| 122 |
The formal design of distributed controllers with dSL and Spin
|
Wachter, Bram De
|
|
2005
|
|
2 |
p. 177-200
|
article
|
| 123 |
The symbiosis of concurrency and verification: teaching and case studies
|
Pedersen, Jan B.
|
|
2017
|
|
2 |
p. 239-277
|
article
|
| 124 |
The verified software repository: a step towards the verifying compiler
|
Bicarregui, J.C.
|
|
2006
|
|
2 |
p. 143-151
|
article
|
| 125 |
Unifying proof methodologies of duration calculus and timed linear temporal logic
|
Liu, Zhiming
|
|
2004
|
|
2 |
p. 140-154
|
article
|
| 126 |
UNITY and Büchi automata
|
Hesselink, Wim H.
|
|
|
|
2 |
p. 185-205
|
article
|
| 127 |
Using probabilistic model checking for dynamic power management
|
Norman, Gethin
|
|
2005
|
|
2 |
p. 160-176
|
article
|
| 128 |
VDM semantics of programming languages: combinators and monads
|
Mosses, Peter D.
|
|
2010
|
|
2 |
p. 221-238
|
article
|
| 129 |
Verification and falsification of programs with loops using predicate abstraction
|
Kroening, Daniel
|
|
2009
|
|
2 |
p. 105-128
|
article
|
| 130 |
Winskel is (almost) Right: Towards a Mechanized Semantics Textbook
|
Nipkow, Tobias
|
|
1998
|
|
2 |
p. 171-186
|
article
|
Journal description