| nr |
titel |
auteur |
tijdschrift |
jaar |
jaarg. |
afl. |
pagina('s) |
type |
| 1 |
A behavioral type system and its application in Ptolemy II
|
Lee, Edward A.
|
|
2004
|
|
3 |
p. 210-237
|
artikel
|
| 2 |
Abstraction and Testing in CSP
|
Schneider, Steve
|
|
2000
|
|
3 |
p. 165-181
|
artikel
|
| 3 |
A comparison of tools for teaching formal software verification
|
Feinerer, Ingo
|
|
2008
|
|
3 |
p. 293-301
|
artikel
|
| 4 |
A Dynamic Logic for deductive verification of multi-threaded programs
|
Beckert, Bernhard
|
|
2012
|
|
3 |
p. 405-437
|
artikel
|
| 5 |
A Formal Definition of Time in LOTOS
|
Léonard, Luc
|
|
1998
|
|
3 |
p. 248-266
|
artikel
|
| 6 |
A Formal Definition of Time in LOTOS
|
Léonard, Luc
|
|
1998
|
|
3 |
p. 248-266
|
artikel
|
| 7 |
A functional formalization of on chip communications
|
Schmaltz, Julien
|
|
2007
|
|
3 |
p. 241-258
|
artikel
|
| 8 |
A generalized semantics of PROMELA for abstract model checking
|
Gallardo, María del Mar
|
|
2004
|
|
3 |
p. 166-193
|
artikel
|
| 9 |
A Hoare logic for linear systems
|
Arthan, Rob
|
|
2011
|
|
3 |
p. 345-363
|
artikel
|
| 10 |
A language-independent proof system for full program equivalence
|
Ciobâcă, Ştefan
|
|
2016
|
|
3 |
p. 469-497
|
artikel
|
| 11 |
Almost ASAP semantics: from timed models to timed implementations
|
Wulf, Martin De
|
|
2005
|
|
3 |
p. 319-341
|
artikel
|
| 12 |
A Mechanically Proved and Incremental Development of IEEE 1394 Tree Identify Protocol
|
Abrial, Jean-Raymond
|
|
2003
|
|
3 |
p. 215-227
|
artikel
|
| 13 |
A Minimal Graphical User Interface for the Jape Proof Calculator
|
Bornat, Richard
|
|
1999
|
|
3 |
p. 244-271
|
artikel
|
| 14 |
A modeling and verification framework for optical quantum circuits
|
Beillahi, Sidi Mohamed
|
|
2019
|
|
3 |
p. 321-351
|
artikel
|
| 15 |
An analysis of refinement in an abortive paradigm
|
Deutsch, Moshe
|
|
2006
|
|
3 |
p. 329-363
|
artikel
|
| 16 |
Angelic nondeterminism in the unifying theories of programming
|
Cavalcanti, Ana
|
|
2006
|
|
3 |
p. 288-307
|
artikel
|
| 17 |
An integrated framework for the performance analysis of asynchronous communicating stochastic processes
|
López, Natalia
|
|
2004
|
|
3 |
p. 238-262
|
artikel
|
| 18 |
An operational semantics for object-oriented concepts based on the class hierarchy
|
Colvin, Robert J.
|
|
2012
|
|
3 |
p. 491-535
|
artikel
|
| 19 |
A program analysis framework for tccp based on abstract interpretation
|
Comini, Marco
|
|
2017
|
|
3 |
p. 531-557
|
artikel
|
| 20 |
Assumption propagation through annotated programs
|
Chaudhari, Dipak L.
|
|
2016
|
|
3 |
p. 495-530
|
artikel
|
| 21 |
Atomicity failure and the retrenchment atomicity pattern
|
Banach, Richard
|
|
2011
|
|
3 |
p. 439-464
|
artikel
|
| 22 |
Automated verification and refinement for physical-layer protocols
|
Brown, Geoffrey M.
|
|
2010
|
|
3 |
p. 243-266
|
artikel
|
| 23 |
Balancing expressiveness in formal approaches to concurrency
|
Jones, Cliff B.
|
|
2014
|
|
3 |
p. 475-497
|
artikel
|
| 24 |
Book Reviews
|
|
|
1998
|
|
3 |
p. 307-310
|
artikel
|
| 25 |
Book Reviews
|
,
|
|
1998
|
|
3 |
p. 307-310
|
artikel
|
| 26 |
Broadcast MSCs
|
Krüger, I.
|
|
2004
|
|
3 |
p. 194-209
|
artikel
|
| 27 |
But What if I Don't Want to Wait Forever?
|
Fidge, Colin
|
|
2003
|
|
3 |
p. 281-294
|
artikel
|
| 28 |
Component-wise incremental LTL model checking
|
Molnár, Vince
|
|
2015
|
|
3 |
p. 345-379
|
artikel
|
| 29 |
Compositional reasoning about active objects with shared futures
|
Din, Crystal Chang
|
|
2014
|
|
3 |
p. 551-572
|
artikel
|
| 30 |
Computing maximal weak and other bisimulations
|
Boulgakov, Alexandre
|
|
2016
|
|
3 |
p. 381-407
|
artikel
|
| 31 |
Concolic testing of the multi-sector read operation for flash storage platform software
|
Kim, Moonzoo
|
|
2011
|
|
3 |
p. 355-374
|
artikel
|
| 32 |
Consistency-preserving refactoring of refinement structures in Event-B models
|
Kobayashi, Tsutomu
|
|
2019
|
|
3 |
p. 287-320
|
artikel
|
| 33 |
Correct-by-construction model driven engineering composition operators
|
Kezadri Hamiaz, Mounira
|
|
2016
|
|
3 |
p. 409-440
|
artikel
|
| 34 |
csp2B: A Practical Approach to Combining CSP and B
|
Butler, Michael
|
|
2000
|
|
3 |
p. 182-198
|
artikel
|
| 35 |
Data Abstraction Techniques in the Validation of CSP-OZ Specifications
|
Wehrheim, Heike
|
|
2000
|
|
3 |
p. 147-164
|
artikel
|
| 36 |
Data refinement and singleton failures refinement are not equivalent
|
Reeves, Steve
|
|
2008
|
|
3 |
p. 295-301
|
artikel
|
| 37 |
Editorial
|
COOKE, JOHN
|
|
2003
|
|
3 |
p. 199
|
artikel
|
| 38 |
Editorial
|
Jones, C. B.
|
|
2014
|
|
3 |
p. 433
|
artikel
|
| 39 |
Editorial
|
Woodcock, Jim
|
|
2012
|
|
3 |
p. 303
|
artikel
|
| 40 |
Editorial
|
Falaschi, Moreno
|
|
2017
|
|
3 |
p. 381-382
|
artikel
|
| 41 |
Editorial
|
Merz, Stephan
|
|
2016
|
|
3 |
p. 343-344
|
artikel
|
| 42 |
Editorial
|
Eleftherakis, George
|
|
2015
|
|
3 |
p. 473
|
artikel
|
| 43 |
Editorial
|
Bowen, Jonathan P.
|
|
2013
|
|
3 |
p. 343
|
artikel
|
| 44 |
Editorial
|
Chen, Xiaoping
|
|
|
|
3 |
p. 299-300
|
artikel
|
| 45 |
Editorial
|
Boca, Paul
|
|
2009
|
|
3 |
p. 225
|
artikel
|
| 46 |
Editorial
|
,
|
|
1999
|
|
3 |
p. 223-224
|
artikel
|
| 47 |
Editorial
|
Cooke, John
|
|
2005
|
|
3 |
p. 259
|
artikel
|
| 48 |
Editorial
|
Broy, Manfred
|
|
2004
|
|
3 |
p. 165
|
artikel
|
| 49 |
Efficient representation of the attacker’s knowledge in cryptographic protocols analysis
|
Bertolotti, Ivan Cibrario
|
|
2008
|
|
3 |
p. 303-348
|
artikel
|
| 50 |
Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving
|
Antonino, Pedro
|
|
2019
|
|
3 |
p. 375-409
|
artikel
|
| 51 |
Elucidating concurrent algorithms via layers of abstraction and reification
|
Jones, Cliff B.
|
|
2010
|
|
3 |
p. 289-306
|
artikel
|
| 52 |
Enhancing Robustness Verification for Deep Neural Networks via Symbolic Propagation
|
Yang, Pengfei
|
|
|
|
3 |
p. 407-435
|
artikel
|
| 53 |
Equational formulas and pattern operations in initial order-sorted algebras
|
Meseguer, José
|
|
2017
|
|
3 |
p. 423-452
|
artikel
|
| 54 |
Exploiting augmented intelligence in the modeling of safety-critical autonomous systems
|
Yang, Zhibin
|
|
|
|
3 |
p. 343-384
|
artikel
|
| 55 |
False Loop Detection in the IEEE 1394 Tree Identify Phase
|
Romijn, Judi
|
|
2003
|
|
3 |
p. 319-327
|
artikel
|
| 56 |
Formalization of Time and Space
|
Hehner, Eric C. R.
|
|
1998
|
|
3 |
p. 290-306
|
artikel
|
| 57 |
Formalization of Time and Space
|
Hehner, Eric C. R.
|
|
1998
|
|
3 |
p. 290-306
|
artikel
|
| 58 |
Formalizing non-interference for a simple bytecode language in Coq
|
Kammüller, Florian
|
|
2007
|
|
3 |
p. 259-275
|
artikel
|
| 59 |
Frama-C: A software analysis perspective
|
Kirchner, Florent
|
|
2015
|
|
3 |
p. 573-609
|
artikel
|
| 60 |
Fun with FireWire: A Comparative Study of Formal Verification Methods Applied to the IEEE 1394 Root Contention Protocol
|
Stoelinga, Mariëlle
|
|
2003
|
|
3 |
p. 328-337
|
artikel
|
| 61 |
Generalised multi-pattern-based verification of programs with linear linked structures
|
Češka, Milan
|
|
2007
|
|
3 |
p. 363-374
|
artikel
|
| 62 |
Guest Editorial
|
Lazic, Ranko
|
|
2007
|
|
3 |
p. 275
|
artikel
|
| 63 |
Guest Editorial Editorial for the FAC Special Issue based on derivative papers from “Refine ’05”
|
Boiten, Eerke
|
|
2006
|
|
3 |
p. 263
|
artikel
|
| 64 |
Heterogeneous Notations for Pure Formal Method Integration
|
Paige, Richard F.
|
|
1998
|
|
3 |
p. 233-242
|
artikel
|
| 65 |
Heterogeneous Notations for Pure Formal Method Integration
|
Paige, Richard F.
|
|
1998
|
|
3 |
p. 233-242
|
artikel
|
| 66 |
IEEE 1394 Tree Identify Protocol: Introduction to the Case Study
|
Maharaj, Savi
|
|
2003
|
|
3 |
p. 200-214
|
artikel
|
| 67 |
Inferring Switched Nonlinear DynamicalSystems
|
Jin, Xiangyu
|
|
|
|
3 |
p. 385-406
|
artikel
|
| 68 |
Interactive Proof Critics
|
Ireland, Andrew
|
|
1999
|
|
3 |
p. 302-325
|
artikel
|
| 69 |
Interactive tool support for CSP || B consistency checking
|
Evans, Neil
|
|
2007
|
|
3 |
p. 277-302
|
artikel
|
| 70 |
Invariant based programming: basic approach and teaching experiences
|
Back, Ralph-Johan
|
|
2008
|
|
3 |
p. 227-244
|
artikel
|
| 71 |
Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example
|
Jones, Cliff B.
|
|
2019
|
|
3 |
p. 353-374
|
artikel
|
| 72 |
John McCarthy (1927–2011)
|
Jones, Cliff B.
|
|
2012
|
|
3 |
p. 305-306
|
artikel
|
| 73 |
John Warner Backus: 3 Dec 1924–17 March 2007
|
Bjørner, Dines
|
|
2008
|
|
3 |
p. 239-240
|
artikel
|
| 74 |
John Warner Backus: 3 Dec 1924–17 March 2007
|
Bjørner, Dines
|
|
|
|
3 |
p. 239-240
|
artikel
|
| 75 |
Knaster-Tarski Revisited
|
Jonker, Jan Eppo
|
|
1998
|
|
3 |
p. 214-232
|
artikel
|
| 76 |
Knaster-Tarski Revisited
|
Jonker, Jan Eppo
|
|
1998
|
|
3 |
p. 214-232
|
artikel
|
| 77 |
Language and tool support for event refinement structures in Event-B
|
Salehi Fathabadi, Asieh
|
|
2014
|
|
3 |
p. 499-523
|
artikel
|
| 78 |
Learning safe neural network controllers with barrier certificates
|
Zhao, Hengjun
|
|
|
|
3 |
p. 437-455
|
artikel
|
| 79 |
LΩUI: Lovely ΩMEGA User Interface
|
Siekmann, Jörg
|
|
1999
|
|
3 |
p. 326-342
|
artikel
|
| 80 |
Machine learning steered symbolic execution framework for complex software code
|
Bu, Lei
|
|
|
|
3 |
p. 301-323
|
artikel
|
| 81 |
Model checking RAISE applicative specifications
|
Perna, Juan I.
|
|
2011
|
|
3 |
p. 365-388
|
artikel
|
| 82 |
Model checking with bounded context switching
|
Holzmann, Gerard J.
|
|
2010
|
|
3 |
p. 365-389
|
artikel
|
| 83 |
Model-driven synthesis of formally precise, stylized software architectures
|
Bagheri, Hamid
|
|
2016
|
|
3 |
p. 441-467
|
artikel
|
| 84 |
Modelling IEEE 802.11 CSMA/CA RTS/CTS with stochastic bigraphs with sharing
|
Calder, Muffy
|
|
2013
|
|
3 |
p. 537-561
|
artikel
|
| 85 |
On dual programs in co-logic programming and the Horn $${\mu}$$μ-calculus
|
Seki, Hirohisa
|
|
2016
|
|
3 |
p. 401-421
|
artikel
|
| 86 |
Operational semantics of resolution and productivity in Horn clause logic
|
Fu, Peng
|
|
2016
|
|
3 |
p. 453-474
|
artikel
|
| 87 |
Optimizing sorting algorithms by using sorting networks
|
Codish, Michael
|
|
2016
|
|
3 |
p. 559-579
|
artikel
|
| 88 |
Partial order semantics for use case and task models
|
Sinnig, Daniel
|
|
2010
|
|
3 |
p. 307-332
|
artikel
|
| 89 |
Practice-oriented courses in formal methods using VDM++
|
Larsen, Peter Gorm
|
|
2008
|
|
3 |
p. 245-257
|
artikel
|
| 90 |
Predicate diagrams for the verification of real-time systems
|
Kang, Eun-Young
|
|
2007
|
|
3 |
p. 401-413
|
artikel
|
| 91 |
Probabilistic Model Checking of Deadline Properties in the IEEE 1394 FireWire Root Contention Protocol
|
Kwiatkowska, Marta
|
|
2003
|
|
3 |
p. 295-318
|
artikel
|
| 92 |
Program verification with interacting analysis plugins
|
Charlton, Nathaniel
|
|
2007
|
|
3 |
p. 375-399
|
artikel
|
| 93 |
Proof checking and logic programming
|
Miller, Dale
|
|
2016
|
|
3 |
p. 383-399
|
artikel
|
| 94 |
Proof producing synthesis of arithmetic and cryptographic hardware
|
Slind, Konrad
|
|
2007
|
|
3 |
p. 343-362
|
artikel
|
| 95 |
Proving as Editing HOL Tactics
|
Takahashi, Koichi
|
|
1999
|
|
3 |
p. 343-357
|
artikel
|
| 96 |
Proving termination of nonlinear command sequences
|
Babić, Domagoj
|
|
2012
|
|
3 |
p. 389-403
|
artikel
|
| 97 |
Ready for testing: ensuring conformance to industrial standards through formal verification
|
Feo-Arenis, Sergio
|
|
2016
|
|
3 |
p. 499-527
|
artikel
|
| 98 |
Reasoning about goal-directed real-time teleo-reactive programs
|
Dongol, Brijesh
|
|
2013
|
|
3 |
p. 563-589
|
artikel
|
| 99 |
Relating Z and First-Order Logic
|
Martin, Andrew P.
|
|
2000
|
|
3 |
p. 199-209
|
artikel
|
| 100 |
Responsiveness and stable revivals
|
Reed, J. N.
|
|
2007
|
|
3 |
p. 303-319
|
artikel
|
| 101 |
SDLV: Verification of Steering Angle Safety for Self-Driving Cars
|
Wu, Huihui
|
|
|
|
3 |
p. 325-341
|
artikel
|
| 102 |
Security analysis of efficient (Un-) fair non-repudiation protocols
|
Gürgens, S.
|
|
2005
|
|
3 |
p. 260-276
|
artikel
|
| 103 |
Semantics of the probabilistic Lambda CalculusBy Dirk Draheim
|
Loreti, Michele
|
|
|
|
3 |
p. 457-458
|
artikel
|
| 104 |
Social and Semiotic Analyses for Theorem Prover User Interface Design 1
|
Goguen, Joseph
|
|
1999
|
|
3 |
p. 272-301
|
artikel
|
| 105 |
Soundness of workflow nets: classification, decidability, and analysis
|
Aalst, W. M. P. van der
|
|
2010
|
|
3 |
p. 333-363
|
artikel
|
| 106 |
Specification and analysis of synchronous reactions
|
Nebut, Mirabelle
|
|
2004
|
|
3 |
p. 263-291
|
artikel
|
| 107 |
Specification and Verification of the Tree Identify Protocol of IEEE 1394 in Rewriting Logic
|
Verdejo, Alberto
|
|
2003
|
|
3 |
p. 228-246
|
artikel
|
| 108 |
Specification of communicating processes: temporal logic versus refusals-based refinement
|
Lowe, Gavin
|
|
2007
|
|
3 |
p. 277-294
|
artikel
|
| 109 |
Strategy based semantics for mobility with time and access permissions
|
Ciobanu, Gabriel
|
|
2014
|
|
3 |
p. 525-549
|
artikel
|
| 110 |
Tank monitoring: a pAMN case study
|
Schneider, Steve
|
|
2006
|
|
3 |
p. 308-328
|
artikel
|
| 111 |
Temporal-logic property preservation under Z refinement
|
Derrick, John
|
|
2011
|
|
3 |
p. 393-416
|
artikel
|
| 112 |
Test generation from state based use case models
|
Nogueira, Sidney
|
|
2012
|
|
3 |
p. 441-490
|
artikel
|
| 113 |
Testing interruptions in reactive systems
|
Andrade, Wilkerson L.
|
|
2011
|
|
3 |
p. 331-353
|
artikel
|
| 114 |
The CtCoq System: Design and Architecture
|
Bertot, Yves
|
|
1999
|
|
3 |
p. 225-243
|
artikel
|
| 115 |
The dynamic frames theory
|
Kassios, I. T.
|
|
2010
|
|
3 |
p. 267-288
|
artikel
|
| 116 |
The Essence of Reynolds
|
Brookes, Stephen
|
|
2014
|
|
3 |
p. 435-439
|
artikel
|
| 117 |
The First World Congress on Formal Methods in the Development of Computing Systems
|
Wing, Jeanette
|
|
2000
|
|
3 |
p. 145-146
|
artikel
|
| 118 |
The Humble Humorous Researcher: A Tribute to Michel Sintzoff
|
Lamsweerde, Axel van
|
|
2011
|
|
3 |
p. 239-242
|
artikel
|
| 119 |
The Humble Humorous Researcher: A Tribute to Michel Sintzoff
|
van Lamsweerde, Axel
|
|
|
|
3 |
p. 239-242
|
artikel
|
| 120 |
The RISC ProofNavigator: a proving assistant for program verification in the classroom
|
Schreiner, Wolfgang
|
|
2008
|
|
3 |
p. 277-291
|
artikel
|
| 121 |
The specification logic νZ
|
Henson, Martin C.
|
|
2006
|
|
3 |
p. 364-395
|
artikel
|
| 122 |
The Standard Logic of Z is Inconsistent
|
Henson, Martin C.
|
|
1998
|
|
3 |
p. 243-247
|
artikel
|
| 123 |
The Standard Logic of Z is Inconsistent
|
Henson, Martin C.
|
|
1998
|
|
3 |
p. 243-247
|
artikel
|
| 124 |
Time-budgeting: a component based development methodology for real-time embedded systems
|
Dixit, Manoj G.
|
|
2013
|
|
3 |
p. 591-621
|
artikel
|
| 125 |
Timed CCP compositionally embeds Argos and Lustre
|
Tini, Simone
|
|
2004
|
|
3 |
p. 292-312
|
artikel
|
| 126 |
Tool support for learning Büchi automata and linear temporal logic
|
Tsay, Yih-Kuen
|
|
2008
|
|
3 |
p. 259-275
|
artikel
|
| 127 |
Towards a Formal Treatment of Implicit Invocation Using Rely/Guarantee Reasoning
|
Dingel, J.
|
|
1998
|
|
3 |
p. 193-213
|
artikel
|
| 128 |
Towards a Formal Treatment of Implicit Invocation Using Rely/Guarantee Reasoning
|
Dingel, J.
|
|
1998
|
|
3 |
p. 193-213
|
artikel
|
| 129 |
Transforming Boolean equalities into constraints
|
Antoy, Sergio
|
|
2016
|
|
3 |
p. 475-494
|
artikel
|
| 130 |
Using fold-in and fold-out in the architecture recovery of software systems
|
Risi, Michele
|
|
2011
|
|
3 |
p. 307-330
|
artikel
|
| 131 |
Using SPIN to Analyse the Tree Identification Phase of the IEEE 1394 High-Performance Serial Bus (FireWire) Protocol
|
Calder, M.
|
|
2003
|
|
3 |
p. 247-266
|
artikel
|
| 132 |
Validating a web service security abstraction by typing
|
Gordon, Andrew D.
|
|
2005
|
|
3 |
p. 277-318
|
artikel
|
| 133 |
Verification of a sliding window protocol in μCRL and PVS
|
Badban, Bahareh
|
|
2005
|
|
3 |
p. 342-388
|
artikel
|
| 134 |
Verification of clock synchronization algorithms: experiments on a combination of deductive tools
|
Barsotti, Damián
|
|
2007
|
|
3 |
p. 321-341
|
artikel
|
| 135 |
Verifying compiled file system code
|
Mühlberg, Jan Tobias
|
|
2011
|
|
3 |
p. 375-391
|
artikel
|
| 136 |
Verifying data refinements using a model checker
|
Smith, Graeme
|
|
2006
|
|
3 |
p. 264-287
|
artikel
|
| 137 |
Verifying the IEEE 1394 FireWire Tree Identify Protocol with SMV
|
Schuppan, Viktor
|
|
2003
|
|
3 |
p. 267-280
|
artikel
|
| 138 |
ZRC – A Refinement Calculus for Z
|
Cavalcanti, Ana
|
|
1998
|
|
3 |
p. 267-289
|
artikel
|
| 139 |
ZRC – A Refinement Calculus for Z
|
Cavalcanti, Ana
|
|
1998
|
|
3 |
p. 267-289
|
artikel
|
Tijdschrift beschrijving