nr |
titel |
auteur |
tijdschrift |
jaar |
jaarg. |
afl. |
pagina('s) |
type |
1 |
Abstract conjunctive partial deduction for the analysis and compilation of coroutines
|
Nys, Vincent |
|
2016 |
|
1 |
p. 125-153 |
artikel |
2 |
Abstractions of non-interference security: probabilistic versus possibilistic
|
Hoang, T. S. |
|
2012 |
|
1 |
p. 169-194 |
artikel |
3 |
A computer checked algebraic verification of a distributed summation algorithm
|
Groote, Jan Friso |
|
2005 |
|
1 |
p. 19-37 |
artikel |
4 |
A data-flow approach to test multi-agent ASMs
|
Cavarra, Alessandra |
|
2009 |
|
1 |
p. 21-41 |
artikel |
5 |
Advanced Features of Duration Calculus and Their Applications in Sequential Hybrid Programs
|
Jifeng, He |
|
2003 |
|
1 |
p. 84-99 |
artikel |
6 |
A formal approach to property testing in causally consistent distributed traces
|
Hallal, H. H. |
|
|
|
1 |
p. 63-83 |
artikel |
7 |
A formal approach to property testing in causally consistent distributed traces
|
Hallal, H. H. |
|
2006 |
|
1 |
p. 63-83 |
artikel |
8 |
A Formal Axiomatization for Alphabet Reasoning with Parametrized Processes
|
Korver, Henri |
|
1998 |
|
1 |
p. 30-42 |
artikel |
9 |
A formal verification technique for behavioural model-to-model transformations
|
Putter, Sander de |
|
2017 |
|
1 |
p. 3-43 |
artikel |
10 |
A framework for model transformation verification
|
Lano, Kevin |
|
2014 |
|
1 |
p. 193-235 |
artikel |
11 |
Algebraic Composition of Function Tables
|
von Mohrenschildt, Martin |
|
2000 |
|
1 |
p. 41-51 |
artikel |
12 |
A Logic for Schema-Based Program Development
|
Henson, Martin C. |
|
2003 |
|
1 |
p. 48-83 |
artikel |
13 |
An algebraic treatment of procedure refinement to support mechanical verification
|
Back, Ralph-Johan |
|
2005 |
|
1 |
p. 69-90 |
artikel |
14 |
Analysing sanity of requirements for avionics systems
|
Barnat, Jiří |
|
2015 |
|
1 |
p. 45-63 |
artikel |
15 |
André Platzer: Logical foundationsof cyber-physical systems
|
Knapp, Alexander |
|
|
|
1 |
p. 149-151 |
artikel |
16 |
An engineering process for the verification of real-time systems
|
Burns, A. |
|
2006 |
|
1 |
p. 111-136 |
artikel |
17 |
An incremental development of the Mondex system in Event-B
|
Butler, Michael |
|
2007 |
|
1 |
p. 61-77 |
artikel |
18 |
ArcAngel: a Tactic Language for Refinement
|
Oliveira, Marcel |
|
2003 |
|
1 |
p. 28-47 |
artikel |
19 |
A semantics comparison workbench for a concurrent, asynchronous, distributed programming language
|
Corrodi, Claudio |
|
2017 |
|
1 |
p. 163-192 |
artikel |
20 |
Atomic actions, and their refinements to isolated protocols
|
Banach, Richard |
|
2009 |
|
1 |
p. 33-61 |
artikel |
21 |
A unification of probabilistic choice within a design-based model of reversible computation
|
Stoddart, Bill |
|
2007 |
|
1 |
p. 107-131 |
artikel |
22 |
A unified integration and component testing approach from deterministic stream X-machine specifications
|
Ipate, Florentin |
|
2015 |
|
1 |
p. 1-20 |
artikel |
23 |
Automating Event-B invariant proofs by rippling and proof patching
|
Lin, Yuhui |
|
2018 |
|
1 |
p. 95-129 |
artikel |
24 |
A Weakness Measure for GR(1) Formulae
|
Cavezza, Davide G. |
|
|
|
1 |
p. 27-63 |
artikel |
25 |
Barrier synchronisation: Axiomatisation and relaxation
|
Stewart, A. |
|
2004 |
|
1 |
p. 36-50 |
artikel |
26 |
Checking noninterference in Timed CSP
|
Roscoe, A. W. |
|
2012 |
|
1 |
p. 3-35 |
artikel |
27 |
Class Refinement as Semantics of Correct Object Substitutability
|
Back, Ralph-Johan |
|
2000 |
|
1 |
p. 18-40 |
artikel |
28 |
Composing and Refining Dense Temporal Logic Specifications
|
Cau, Antonio |
|
2000 |
|
1 |
p. 52-70 |
artikel |
29 |
Compositional noninterference from first principles
|
Morgan, Carroll |
|
2010 |
|
1 |
p. 3-26 |
artikel |
30 |
Computing Permutation Encodings
|
Leino, K. Rustan M. |
|
1999 |
|
1 |
p. 56-74 |
artikel |
31 |
Computing Permutation Encodings
|
Leino, K. Rustan M. |
|
1999 |
|
1 |
p. 56-74 |
artikel |
32 |
Constraint logic programming with a relational machine
|
Gallego Arias, Emilio Jesús |
|
2016 |
|
1 |
p. 97-124 |
artikel |
33 |
Constructing checking sequences for distributed testing
|
Ural, Hasan |
|
|
|
1 |
p. 84-101 |
artikel |
34 |
Constructing checking sequences for distributed testing
|
Ural, Hasan |
|
2006 |
|
1 |
p. 84-101 |
artikel |
35 |
Contract-based verification of MATLAB-style matrix programs
|
Wiik, Jonatan |
|
2016 |
|
1 |
p. 79-107 |
artikel |
36 |
Correction to: Multiple model synchronizationwith multiary delta lenses with amendment andK-Putput
|
Diskin, Zinovy |
|
|
|
1 |
p. 153 |
artikel |
37 |
Cryptographic protocols with everyday objects
|
Heather, James |
|
2013 |
|
1 |
p. 37-62 |
artikel |
38 |
Cut branches before looking for bugs: certifiably sound verification on relaxed slices
|
Léchenet, Jean-Christophe |
|
2017 |
|
1 |
p. 107-131 |
artikel |
39 |
Deciding probabilistic automata weak bisimulation: theory and practice
|
Ferrer Fioriti, Luis María |
|
2016 |
|
1 |
p. 109-143 |
artikel |
40 |
Denotational semantics and its algebraic derivation for an event-driven system-level language
|
Zhu, H. |
|
2014 |
|
1 |
p. 133-166 |
artikel |
41 |
Disciplined, efficient, generalised folds for nested datatypes
|
Martin, Clare |
|
2004 |
|
1 |
p. 19-35 |
artikel |
42 |
Discovering applications of higher order functions through proof planning
|
Cook, A. |
|
2005 |
|
1 |
p. 38-57 |
artikel |
43 |
Dynamical Quantities in Net Systems
|
Genrich, Hartmann J. |
|
2002 |
|
1 |
p. 55-89 |
artikel |
44 |
Editorial
|
Boiten, Eerke |
|
2011 |
|
1 |
p. 1 |
artikel |
45 |
Editorial
|
COOKE, JOHN |
|
2002 |
|
1 |
p. 1 |
artikel |
46 |
Editorial
|
Börger, Egon |
|
2010 |
|
1 |
p. 1-2 |
artikel |
47 |
Editorial
|
Proietti, Maurizio |
|
2016 |
|
1 |
p. 1-2 |
artikel |
48 |
Editorial
|
Denney, Ewen |
|
2017 |
|
1 |
p. 1 |
artikel |
49 |
Editorial
|
Boiten, Eerke |
|
2013 |
|
1 |
p. 1-2 |
artikel |
50 |
Editorial
|
Fränzle, Martin |
|
2019 |
|
1 |
p. 1 |
artikel |
51 |
Editorial
|
Jones, Cliff |
|
2007 |
|
1 |
p. 1-3 |
artikel |
52 |
Editorial
|
Boiten, Eerke |
|
2009 |
|
1 |
p. 1 |
artikel |
53 |
Editorial
|
Cooke, John |
|
2007 |
|
1 |
p. 1 |
artikel |
54 |
Editorial
|
Jones, Cliff |
|
2004 |
|
1 |
p. 1 |
artikel |
55 |
Editorial
|
de Vink, Erik |
|
|
|
1 |
p. 1-2 |
artikel |
56 |
Emergence and refinement
|
Sanders, J. W. |
|
2011 |
|
1 |
p. 45-65 |
artikel |
57 |
ERC – An object-oriented refinement calculus for Eiffel
|
Paige, Richard F. |
|
2004 |
|
1 |
p. 51-79 |
artikel |
58 |
Example Verifications Using Alphabet Axioms
|
Korver, Henri |
|
1998 |
|
1 |
p. 43-58 |
artikel |
59 |
Experiments in program verification using Event-B
|
Hallerstede, Stefan |
|
2011 |
|
1 |
p. 97-125 |
artikel |
60 |
Extensional Petri net
|
Dong, Xiaoju |
|
2018 |
|
1 |
p. 47-58 |
artikel |
61 |
Formal analysis of the compact positionreporting algorithm
|
Dutle, Aaron |
|
|
|
1 |
p. 65-86 |
artikel |
62 |
Formalizing a hierarchical file system
|
Hesselink, Wim H. |
|
2010 |
|
1 |
p. 27-44 |
artikel |
63 |
Formal Methods Europe Update
|
Fitzgerald, John S. |
|
2004 |
|
1 |
p. 2-3 |
artikel |
64 |
Formal probabilistic analysis of detection properties in wireless sensor networks
|
Elleuch, Maissa |
|
2014 |
|
1 |
p. 79-102 |
artikel |
65 |
Formal reliability analysis of redundancy architectures
|
Bozzano, Marco |
|
2019 |
|
1 |
p. 59-94 |
artikel |
66 |
Formal reliability and failure analysis of ethernet based communication networks in a smart grid substation
|
Ahmad, Waqar |
|
|
|
1 |
p. 71-111 |
artikel |
67 |
Formal techniques for performance analysis: blending SAN and PEPA
|
Hillston, Jane |
|
2006 |
|
1 |
p. 3-33 |
artikel |
68 |
Formal verification of security protocol implementations: a survey
|
Avalle, Matteo |
|
2012 |
|
1 |
p. 99-123 |
artikel |
69 |
From MC/DC to RC/DC: formalization and analysis of control-flow testing criteria
|
Vilkomir, Sergiy A. |
|
|
|
1 |
p. 42-62 |
artikel |
70 |
From MC/DC to RC/DC: formalization and analysis of control-flow testing criteria
|
Vilkomir, Sergiy A. |
|
2006 |
|
1 |
p. 42-62 |
artikel |
71 |
Generating tests from B specifications and dynamic selection criteria
|
Julliand, Jacques |
|
2009 |
|
1 |
p. 3-19 |
artikel |
72 |
Generation of complete test suites from mealy input/output transition systems
|
Paiva, Sofia Costa |
|
2015 |
|
1 |
p. 65-78 |
artikel |
73 |
Gerard O’Regan: Concise Guide to FormalMethods: Theory, Fundamentals and IndustryApplications
|
Bowen, Jonathan P. |
|
|
|
1 |
p. 147-148 |
artikel |
74 |
GPU-accelerated steady-state computation of large probabilistic Boolean networks
|
Mizera, Andrzej |
|
2018 |
|
1 |
p. 27-46 |
artikel |
75 |
Guest Editorial
|
Derrick, J. |
|
|
|
1 |
p. 1-2 |
artikel |
76 |
Guest Editorial
|
Derrick, J. |
|
2006 |
|
1 |
p. 1-2 |
artikel |
77 |
Inductive study of confidentiality: for everyone
|
Bella, Giampaolo |
|
2012 |
|
1 |
p. 3-36 |
artikel |
78 |
Integrating stochastic reasoning into Event-B development
|
Tarasyuk, Anton |
|
2014 |
|
1 |
p. 53-77 |
artikel |
79 |
Integration of UML and VHDL-AMS for analogue system modelling
|
Carr, C. T. |
|
2004 |
|
1 |
p. 80-94 |
artikel |
80 |
Invariant-based reasoning about parameterized security protocols
|
Mooij, Arjan J. |
|
2009 |
|
1 |
p. 63-81 |
artikel |
81 |
Invariant diagrams with data refinement
|
Preoteasa, Viorel |
|
2011 |
|
1 |
p. 67-95 |
artikel |
82 |
Linearizability on hardware weak memory models
|
Smith, Graeme |
|
|
|
1 |
p. 1-32 |
artikel |
83 |
Local Invariance
|
Pitt, David H. |
|
2002 |
|
1 |
p. 35-54 |
artikel |
84 |
Maximal incompleteness as obfuscation potency
|
Giacobazzi, Roberto |
|
2016 |
|
1 |
p. 3-31 |
artikel |
85 |
Mechanised support for sound refinement tactics
|
Zeyda, Frank |
|
2011 |
|
1 |
p. 127-160 |
artikel |
86 |
Mechanising Mondex with Z/Eves
|
Freitas, Leo |
|
2007 |
|
1 |
p. 117-139 |
artikel |
87 |
Mechanizing compositional reasoning for concurrent systems: some lessons
|
Ehmety, Sidi O. |
|
2005 |
|
1 |
p. 58-68 |
artikel |
88 |
Minimal refinements of specifications in model and termporal logics
|
Gorogiannis, Nikos |
|
2006 |
|
1 |
p. 35-62 |
artikel |
89 |
Model-based testing of probabilistic systems
|
Gerhold, Marcus |
|
2017 |
|
1 |
p. 77-106 |
artikel |
90 |
Modeling and enhancement of the IEEE 802.11 RTS/CTS scheme in an error-prone channel
|
Yazid, Mohand |
|
2014 |
|
1 |
p. 33-52 |
artikel |
91 |
Modeling and validating Mondex scenarios described in UML and OCL with USE
|
Kuhlmann, Mirco |
|
2007 |
|
1 |
p. 79-100 |
artikel |
92 |
Modeling and Verification of A Timing Protection Mechanism in the OSEK/VDX OS using CSP
|
Huang, Yanhong |
|
|
|
1 |
p. 113-145 |
artikel |
93 |
Modeling layered distributed communication systems
|
Herzberg, D. |
|
2004 |
|
1 |
p. 1-18 |
artikel |
94 |
Modular verification of programs with effectsand effects handlers
|
Letan, Thomas |
|
|
|
1 |
p. 127-150 |
artikel |
95 |
Mondex, an electronic purse: specification and refinement checks with the Alloy model-finding method
|
Ramananandro, Tahina |
|
2007 |
|
1 |
p. 21-39 |
artikel |
96 |
Online First Publication
|
Jones, C.B. |
|
2004 |
|
1 |
p. 4 |
artikel |
97 |
On proving confluence modulo equivalence for Constraint Handling Rules
|
Christiansen, Henning |
|
2016 |
|
1 |
p. 57-95 |
artikel |
98 |
On the purpose of Event-B proof obligations
|
Hallerstede, Stefan |
|
2009 |
|
1 |
p. 133-150 |
artikel |
99 |
On the Use of Data Refinement in the Development of Secure Communications Systems
|
Butler, Michael |
|
2002 |
|
1 |
p. 2-34 |
artikel |
100 |
Optimal and robust controller synthesis using energytimed automata with uncertainty
|
Bacci, Giovanni |
|
|
|
1 |
p. 3-25 |
artikel |
101 |
Parametric probabilistic transition systems for system design and analysis
|
Lanotte, Ruggero |
|
2006 |
|
1 |
p. 93-109 |
artikel |
102 |
Partial evaluation of string obfuscations for Java malware detection
|
Chawdhary, Aziem |
|
2016 |
|
1 |
p. 33-55 |
artikel |
103 |
Partiality and Nondeterminacy in Program Proofs
|
Morris, Joseph M. |
|
1998 |
|
1 |
p. 76-96 |
artikel |
104 |
Preface
|
|
|
2012 |
|
1 |
p. 1-2 |
artikel |
105 |
Presheaves as Configured Specifications
|
Vickers, Steven |
|
2001 |
|
1 |
p. 32-49 |
artikel |
106 |
Probabilistic Duration Calculus for Continuous Time
|
Van Hung, Dang |
|
1999 |
|
1 |
p. 21-44 |
artikel |
107 |
Probabilistic Duration Calculus for Continuous Time
|
Van Hung, Dang |
|
1999 |
|
1 |
p. 21-44 |
artikel |
108 |
ProFeat: feature-oriented engineering for family-based probabilistic model checking
|
Chrszon, Philipp |
|
2017 |
|
1 |
p. 45-75 |
artikel |
109 |
Program Algebra for Component Code
|
Bergstra, J. A. |
|
2000 |
|
1 |
p. 1-17 |
artikel |
110 |
Protective Interface Specifications
|
Leavens, Gary T. |
|
1998 |
|
1 |
p. 59-75 |
artikel |
111 |
Proving completeness of logic programs with the cut
|
Drabent, Włodzimierz |
|
2016 |
|
1 |
p. 155-172 |
artikel |
112 |
Proving linearizability with temporal logic
|
Bäumler, Simon |
|
2009 |
|
1 |
p. 91-112 |
artikel |
113 |
Refinement algebra for probabilistic programs
|
Meinicke, Larissa |
|
2009 |
|
1 |
p. 3-31 |
artikel |
114 |
Retrenchment for Event-B: UseCase-wise development and Rodin integration
|
Banach, Richard |
|
2009 |
|
1 |
p. 113-131 |
artikel |
115 |
Safe abstractions of data encodings in formal security protocol models
|
Pironti, Alfredo |
|
2012 |
|
1 |
p. 125-167 |
artikel |
116 |
SCTL-MUS: A Formal Methodology for Software Development of Distributed Systems. A Case Study
|
Pazos Arias, José J. |
|
2001 |
|
1 |
p. 50-91 |
artikel |
117 |
Security invariants in discrete transition systems
|
Hoang, Thai Son |
|
2012 |
|
1 |
p. 59-87 |
artikel |
118 |
Semantic inheritance in unifying theories of programming
|
Chen, Yifeng |
|
2007 |
|
1 |
p. 89-106 |
artikel |
119 |
Simulation testing of automata
|
Stannett, Mike |
|
|
|
1 |
p. 31-41 |
artikel |
120 |
Simulation testing of automata
|
Stannett, Mike |
|
2006 |
|
1 |
p. 31-41 |
artikel |
121 |
Specification, proof, and model checking of the Mondex electronic purse using RAISE
|
George, Chris |
|
2007 |
|
1 |
p. 101-116 |
artikel |
122 |
Stepwise development and model checking of adistributed interlocking system using RAISE
|
Geisler, S. |
|
|
|
1 |
p. 87-125 |
artikel |
123 |
Stream-Based Specification of Mobile Systems
|
Grosu, Radu |
|
2001 |
|
1 |
p. 1-31 |
artikel |
124 |
Structural Refinement of Systems Specified in Object-Z and CSP
|
Derrick, John |
|
2003 |
|
1 |
p. 1-27 |
artikel |
125 |
Superposition: composition vs refinement of non-deterministic, action-based systems
|
Lopes, Antónia |
|
2004 |
|
1 |
p. 5-18 |
artikel |
126 |
Synthesizing bounded-time 2-phase fault recovery
|
Bonakdarpour, Borzoo |
|
2014 |
|
1 |
p. 1-31 |
artikel |
127 |
Synthesizing structural and behavioral control for reconfigurations in component-based systems
|
Khakpour, Narges |
|
2015 |
|
1 |
p. 21-43 |
artikel |
128 |
Testing methods for X-machines: a review
|
Bogdanov, K. |
|
|
|
1 |
p. 3-30 |
artikel |
129 |
Testing methods for X-machines: a review
|
Bogdanov, K. |
|
2006 |
|
1 |
p. 3-30 |
artikel |
130 |
The certification of the Mondex electronic purse to ITSEC Level E6
|
Woodcock, Jim |
|
2007 |
|
1 |
p. 5-19 |
artikel |
131 |
The Changing Face of Standardization: A Place for Formal Methods?
|
Duce, David |
|
1999 |
|
1 |
p. 1-20 |
artikel |
132 |
The Changing Face of Standardization: A Place for Formal Methods?
|
Duce, David |
|
1999 |
|
1 |
p. 1-20 |
artikel |
133 |
The Least Conjunctive Refinement and Promotion in the Refinement Calculus
|
Mahony, Brendan P. |
|
1999 |
|
1 |
p. 75-105 |
artikel |
134 |
The Least Conjunctive Refinement and Promotion in the Refinement Calculus
|
Mahony, Brendan P. |
|
1999 |
|
1 |
p. 75-105 |
artikel |
135 |
The Safety-Critical Java memory model formalised
|
Cavalcanti, Ana |
|
2012 |
|
1 |
p. 37-57 |
artikel |
136 |
The Verified Incremental Design of a Distributed Spanning Tree Algorithm: Extended Abstract
|
Hesselink, Wim H. |
|
1999 |
|
1 |
p. 45-55 |
artikel |
137 |
The Verified Incremental Design of a Distributed Spanning Tree Algorithm: Extended Abstract
|
Hesselink, Wim H. |
|
1999 |
|
1 |
p. 45-55 |
artikel |
138 |
Toward automatic verification of quantum programs
|
Ying, Mingsheng |
|
2018 |
|
1 |
p. 3-25 |
artikel |
139 |
Unification of Four Versions of Program Semantics
|
Rewitzky, Ingrid |
|
1998 |
|
1 |
p. 1-29 |
artikel |
140 |
Unifying theories in ProofPower-Z
|
Oliveira, Marcel |
|
2007 |
|
1 |
p. 133-158 |
artikel |
141 |
Using Event-B to construct instruction set architectures
|
Wright, Stephen |
|
2010 |
|
1 |
p. 73-89 |
artikel |
142 |
Using formal reasoning on a model of tasks for FreeRTOS
|
Cheng, Shu |
|
2014 |
|
1 |
p. 167-192 |
artikel |
143 |
Using formal verification to evaluate theexecution time of Spark applications
|
Baresi, L. |
|
|
|
1 |
p. 33-70 |
artikel |
144 |
Variability-based model transformation: formal foundation and application
|
Strüber, D. |
|
2017 |
|
1 |
p. 133-162 |
artikel |
145 |
Verification of distributed systems with the axiomatic system of MSVL
|
Ma, Qian |
|
2014 |
|
1 |
p. 103-131 |
artikel |
146 |
Verification of $${{EB}^3}$$EB3 specifications using CADP
|
Vekris, Dimitris |
|
2016 |
|
1 |
p. 145-178 |
artikel |
147 |
Verification of Mondex electronic purses with KIV: from transactions to a security protocol
|
Haneberg, Dominik |
|
2007 |
|
1 |
p. 41-59 |
artikel |
148 |
Verifying anonymity in voting systems using CSP
|
Moran, Murat |
|
2012 |
|
1 |
p. 63-98 |
artikel |
149 |
Verifying a signature architecture: a comparative case study
|
Basin, David |
|
2007 |
|
1 |
p. 63-91 |
artikel |
150 |
Z2SAL: a translation-based model checker for Z
|
Derrick, John |
|
2009 |
|
1 |
p. 43-71 |
artikel |