|
|
Gethin Norman: Publications
by date |
by title |
by type |
bibtex
|
[1]
|
Abstraction Refinement for Probabilistic Software
M. Kattenbelt, M. Kwiatkowska, G. Norman, D. Parker
In Proc. 10th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'09) Springer, January 2009.
Details
|
BibTeX
|
|
[2]
|
Probabilistic model checking of complex biological pathways
J. Heath et al.
Theoretical Computer Science, Vol. 319, pages 239-257. 2008.
Details
|
BibTeX
| Link (pdf) |
|
[3]
|
Game-Based Probabilistic Predicate Abstraction in PRISM
M. Kattenbelt et al.
In Proc. 6th Workshop on Quantitative Aspects of Programming Languages (QAPL'08) 2008.
Details
|
BibTeX
| Link (pdf) |
|
[4]
|
Game-Based Probabilistic Predicate Abstraction in PRISM
M. Kattenbelt et al.
No. RR-08-01, Technical Report, Oxford University Computing Laboratory. February 2008.
Details
|
BibTeX
| Download (pdf) |
|
[5]
|
A Game-based Abstraction-Refinement Framework for Markov Decision Processes
M. Kattenbelt et al.
No. RR-08-06, Technical Report, Oxford University Computing Laboratory. February 2008.
Details
|
BibTeX
| Download (pdf) |
|
[6]
|
Symbolic Model Checking for Probabilistic Timed Automata
M. Kwiatkowska et al.
Information and Computation, Vol. 205, No. 7, pages 1027-1077. 2007.
Details
|
BibTeX
| Link (pdf) |
|
[7]
|
Stochastic Model Checking
M. Kwiatkowska, G. Norman and D. Parker
In M. Bernardo, J. Hillston, editors, Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM'07) Vol. 4486 of LNCS (Tutorial Volume), pages 220-270. Springer, 2007.
Details
|
BibTeX
| Link (pdf) |
|
[8]
|
Practical Applications of Probabilistic Model Checking to Communication Protocols
M. Duflot et al.
In Handbook of Formal Methods in Industrial Critical Systems 2007.
To appear.
Details
|
BibTeX
|
|
[9]
|
Analysis of Probabilistic Contract Signing
Gethin Norman, Vitaly Shmatikov
2006.
Details
|
BibTeX
|
|
[10]
|
Analysis of Probabilistic Contract Signing
Gethin Norman, Vitaly Shmatikov
Journal of Computer Security, Vol. 14, No. 6, pages 561-589. November 2006.
Details
|
BibTeX
| Link (pdf) |
|
[11]
|
Numerical vs. Statistical Probabilistic Model Checking
H. Younes et al.
International Journal on Software Tools for Technology Transfer (STTT), Vol. 8, No. 3, pages 216-228. 2006.
Details
|
BibTeX
| Link (pdf) |
|
[12]
|
A Formal Analysis of Bluetooth Device Discovery
M. Duflot et al.
Int. Journal on Software Tools for Technology Transfer, Vol. 8, No. 6, pages 621—632. 2006.
Details
|
BibTeX
| Link (pdf) |
|
[13]
|
Performance Analysis of Probabilistic Timed Automata using Digital Clocks
M. Kwiatkowska et al.
Formal Methods in System Design, Vol. 29, pages 33-78. 2006.
Details
|
BibTeX
| Link (pdf) |
|
[14]
|
Controller Dependability Analysis By Probabilistic Model Checking
M. Kwiatkowska, G. Norman and D. Parker
Control Engineering Practice, Vol. 15, No. 11, pages 1427-1434. 2006.
Details
|
BibTeX
| Link (pdf) |
|
[15]
|
Model Checking Expected Time and Expected Reward Formulae with Random Time Bounds
M. Kwiatkowska, G. Norman and A. Pacheco
Computers & Mathematics with Applications, Vol. 51, No. 2, pages 305-316. 2006.
Details
|
BibTeX
| Link (pdf) |
|
[16]
|
PRISM: A Tool for Automatic Verification of Probabilistic Systems
A. Hinton et al.
In H. Hermanns, J. Palsberg, editors, Proc. 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06) Vol. 3920 of LNCS, pages 441-444. Springer, 2006.
Details
|
BibTeX
| Link (pdf) |
|
[17]
|
Symmetry Reduction for Probabilistic Model Checking
M. Kwiatkowska, G. Norman and D. Parker
In T. Ball, R. Jones, editors, Proc. 18th International Conference on Computer Aided Verification (CAV'06) Vol. 4114 of LNCS, pages 234-248. Springer, 2006.
Details
|
BibTeX
| Link (pdf) |
|
[18]
|
Simulation and verification for computational modelling of signalling pathways
M. Kwiatkowska et al.
In L. F. Perrone et al. , editors, Proc. Winter Simulation Conference pages 1666—1675. Omnipress, 2006.
Details
|
BibTeX
| Link (pdf) |
|
[19]
|
Probabilistic model checking of complex biological pathways
J. Heath et al.
In C. Priami, editor, Proc. Computational Methods in Systems Biology (CMSB'06) Vol. 4210 of Lecture Notes in Bioinformatics, pages 32—47. Springer Verlag, 2006.
Details
|
BibTeX
| Link (pdf) |
|
[20]
|
Probabilistic Mobile Ambients
M. Kwiatkowska et al.
No. CSR-06-09, Technical Report, University of Birmingham, School of Computer Science. 2006.
Details
|
BibTeX
| Link (pdf) |
|
[21]
|
On reduction criteria for probabilistic reward models
M. Größer et al.
In S. Arun-Kumar, N. Garg, editors, Proc. 25th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'06) Vol. 4337 of LNCS, pages 309-320. Springer, 2006.
Details
|
BibTeX
| Link (pdf) |
|
[22]
|
Game-based Abstraction for Markov Decision Processes
M. Kwiatkowska, G. Norman and D. Parker
No. CSR-06-05, Technical Report, School of Computer Science, University of Birmingham. 2006.
Details
|
BibTeX
| Link (pdf) |
|
[23]
|
Game-based Abstraction for Markov Decision Processes
M. Kwiatkowska, G. Norman and D. Parker
In Proc. 3rd International Conference on Quantitative Evaluation of Systems (QEST'06) pages 157-166. IEEE CS Press, 2006.
Details
|
BibTeX
| Link (pdf) |
|
[24]
|
Evaluating the Reliability of NAND Multiplexing with PRISM
G. Norman et al.
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 24, No. 10, pages 1629-1637. October 2005.
Details
|
BibTeX
| Link (pdf) |
|
[25]
|
Using Probabilistic Model Checking for Dynamic Power Management
G. Norman et al.
Formal Aspects of Computing, Vol. 17, No. 2, pages 160-176. 2005.
Details
|
BibTeX
| Link (pdf) |
|
[26]
|
Quantitative analysis with the probabilistic model checker PRISM
M. Kwiatkowska, G. Norman and D. Parker
Electronic Notes in Theoretical Computer Science, Vol. 153, No. 2, pages 5-31. 2005.
Details
|
BibTeX
| Link (pdf) |
|
[27]
|
Probabilistic model checking in practice: Case studies with PRISM
M. Kwiatkowska, G. Norman and D. Parker
ACM SIGMETRICS Performance Evaluation Review, Vol. 32, No. 4, pages 16—21. March 2005.
Details
|
BibTeX
| Link (pdf) |
|
[28]
|
Stochastic transition systems for continuous state spaces and non-determinism
S. Cattani et al.
In V. Sassone, editor, Proc. Foundations of Software Science and Computation Structures (FOSSACS'05) Vol. 3441 of Lecture Notes in Computer Science, pages 125—139. Springer Verlag, 2005.
Details
|
BibTeX
| Link (pdf) |
|
[29]
|
Probabilistic Model Checking and Power-Aware Computing
M. Kwiatkowska, G. Norman and D. Parker
In Proc. 7th International Workshop on Performability Modeling of Computer and Communication Systems (PMCCS'05) pages 6—9. 2005.
Details
|
BibTeX
| Link (pdf) |
|
[30]
|
Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach
M. Kwiatkowska, G. Norman and D. Parker
International Journal on Software Tools for Technology Transfer (STTT), Vol. 6, No. 2, pages 128—142. 2004.
Details
|
BibTeX
| Link (pdf) |
|
[31]
|
Automatic Verification of the IEEE 1394 Root Contention Protocol with KRONOS and PRISM
C. Daws, M. Kwiatkowska and G. Norman
International Journal on Software Tools for Technology Transfer (STTT), Vol. 5, No. 2--3, pages 221—236. 2004.
Details
|
BibTeX
| Link (pdf) |
|
[32]
|
PRISM 2.0: A Tool for Probabilistic Model Checking
M. Kwiatkowska, G. Norman and D. Parker
In Proc. 1st International Conference on Quantitative Evaluation of Systems (QEST'04) pages 322—323. IEEE Computer Society Press, 2004.
Details
|
BibTeX
| Link (pdf) |
|
[33]
|
Symbolic Model Checking for Probabilistic Timed Automata
M. Kwiatkowska et al.
In Y. Lakhnech, S. Yovine, editors, Proc. Joint Conference on Formal Modelling and Analysis of Timed Systems and Formal Techniques in Real-Time and Fault Tolerant Systems (FORMATS/FTRTFT'04) Vol. 3253 of LNCS, pages 293—308. Springer, 2004.
Details
|
BibTeX
| Link (pdf) |
|
[34]
|
Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study
H. Younes et al.
In K. Jensen, A. Podelski, editors, Proc. 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'04) Vol. 2988 of LNCS, pages 46—60. Springer, 2004.
Details
|
BibTeX
| Link (pdf) |
|
[35]
|
Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems, P. Panangaden and F. van Breugel (eds.)
J. Rutten et al.
Vol. 23 of CRM Monograph Series. American Mathematical Society. 2004.
Details
|
BibTeX
|
|
[36]
|
Evaluating the Reliability of Defect-Tolerant Architectures for Nanotechnology with Probabilistic Model Checking
G. Norman et al.
In Proc. International Conference on VLSI Design (VSLI'04) pages 907-914. IEEE Computer Society Press, 2004.
Details
|
BibTeX
| Link (pdf) |
|
[37]
|
Controller Dependability Analysis By Probabilistic Model Checking
M. Kwiatkowska, G. Norman and D. Parker
In Proc. 11th IFAC Symposium on Information Control Problems in Manufacturing (INCOM'04) 2004.
Details
|
BibTeX
| Link (pdf) |
|
[38]
|
A Formal Analysis of Bluetooth Device Discovery
M. Duflot et al.
In Proc. 1st International Symposium on Leveraging Applications of Formal Methods (ISOLA'04) 2004.
Details
|
BibTeX
| Link (pdf) |
|
[39]
|
On the use of MTBDDs for Performability Analysis and Verification of Stochastic Systems
H. Hermanns et al.
Journal of Logic and Algebraic Programming: Special Issue on Probabilistic Techniques for the Design and Analysis of Systems, Vol. 56, No. 1-2, pages 23—67. 2003.
Details
|
BibTeX
| Link (pdf) |
|
[40]
|
Probabilistic Model Checking of Deadline Properties in the IEEE 1394 FireWire Root Contention Protocol
M. Kwiatkowska, G. Norman and J. Sproston
Formal Aspects of Computing, Vol. 14, No. 3, pages 295—318. 2003.
Details
|
BibTeX
| Link (pdf) |
|
[41]
|
Using Probabilistic Model Checking for Dynamic Power Management
G. Norman et al.
In M. Leuschel, S. Gruner and S. Lo Presti, editors, Proc. 3rd Workshop on Automated Verification of Critical Systems (AVoCS'03) pages 202—215. 2003.
Details
|
BibTeX
| Link (pdf) |
|
[42]
|
Symbolic Model Checking for Probabilistic Timed Automata
M. Kwiatkowska, G. Norman and J. Sproston
No. CSR-03-10, Technical Report, School of Computer Science, University of Birmingham. 2003.
Details
|
BibTeX
| Link (pdf) |
|
[43]
|
Symbolic Computation of Minimal Probabilistic Reachability
M. Kwiatkowska, G. Norman and J. Sproston
No. CSR-03-01, Technical Report, University of Birmingham, School of Computer Science. January 2003.
Details
|
BibTeX
| Link (pdf) |
|
[44]
|
Performance Analysis of Probabilistic Timed Automata using Digital Clocks
M. Kwiatkowska et al.
In K. Larsen, P. Niebert, editors, Proc. Formal Modeling and Analysis of Timed Systems (FORMATS'03) Vol. 2791 of LNCS, pages 105—120. Springer-Verlag, September 2003.
Details
|
BibTeX
| Link (pdf) |
|
[45]
|
PCTL model checking of symbolic probabilistic systems
Marta Z Kwiatkowska, Gethin Norman and Jeremy Sproston
No. CSR-03-2, Technical Report, University of Birmingham, School of Computer Science. 2003.
Details
|
BibTeX
| Link (pdf) |
|
[46]
|
Automatic Verification of Real-time Systems with Discrete Probability Distributions
M. Kwiatkowska et al.
Theoretical Computer Science, Vol. 282, pages 101—150. June 2002.
Details
|
BibTeX
| Link (pdf) |
|
[47]
|
PRISM: Probabilistic Symbolic Model Checker
M. Kwiatkowska, G. Norman and D. Parker
In T. Field et al. , editors, Proc. 12th International Conference on Modelling Techniques and Tools for Computer Performance Evaluation (TOOLS'02) Vol. 2324 of LNCS, pages 200—204. Springer, 2002.
Details
|
BibTeX
| Link (pdf) |
|
[48]
|
Verifying Randomized Byzantine Agreement
M. Kwiatkowska, G. Norman
In D. Peled, M. Vardi, editors, Proc. Formal Techniques for Networked and Distributed Systems (FORTE'02) Vol. 2529 of LNCS, pages 194—209. Springer, 2002.
Details
|
BibTeX
| Link (pdf) |
|
[49]
|
Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach
M. Kwiatkowska, G. Norman and D. Parker
In J.-P. Katoen, P. Stevens, editors, Proc. 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'02) Vol. 2280 of LNCS, pages 52—66. Grenoble. 2002. Springer.
Details
|
BibTeX
| Link (pdf) |
|
[50]
|
Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol
M. Kwiatkowska, G. Norman and J. Sproston
In H. Hermanns, R. Segala, editors, Proc. 2nd Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM/PROBMIV'02) Vol. 2399 of LNCS, pages 169—187. Springer, 2002.
Details
|
BibTeX
| Link (pdf) |
|
[51]
|
Model Checking CSL Until Formulae with Random Time Bounds
M. Kwiatkowska, G. Norman and A. Pacheco
In H. Hermanns, R. Segala, editors, Proc. 2nd Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM/PROBMIV'02) Vol. 2399 of LNCS, pages 152—168. Springer, 2002.
Details
|
BibTeX
| Link (pdf) |
|
[52]
|
Model Checking Expected Time and Expected Reward Formulae with Random Time Bounds
M. Kwiatkowska, G. Norman and A. Pacheco
In Proc. 2nd Euro-Japanese Workshop on Stochastic Risk Modelling for Finance, Insurance, Production and Reliability September 2002.
Details
|
BibTeX
| Link (pdf) |
|
[53]
|
Formal Analysis and Validation of Continuous Time Markov Chain Based System Level Power Management Strategies
G. Norman et al.
In W. Rosenstiel, editor, Proc. 7th Annual IEEE International Workshop on High Level Design Validation and Test (HLDVT'02) pages 45—50. IEEE Computer Society Press, October 2002.
Details
|
BibTeX
| Link (pdf) |
|
[54]
|
Automatic Verification of the IEEE 1394 Root Contention Protocol with KRONOS and PRISM
C. Daws, M. Kwiatkowska and G. Norman
In R. Cleaveland, H. Garavel, editors, Proc. 7th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'02) Vol. 66.2 of Electronic Notes in Theoretical Computer Science. Elsevier, 2002.
Details
|
BibTeX
| Link (pdf) |
|
[55]
|
A Symbolic Out-of-Core Solution Method for Markov Models
M. Kwiatkowska et al.
In Proc. Workshop on Parallel and Distributed Model Checking (PDMC'02) Vol. 68.4 of Electronic Notes in Theoretical Computer Science. Elsevier, August 2002.
Details
|
BibTeX
| Link (pdf) |
|
[56]
|
PRISM: Probabilistic Symbolic Model Checker
M. Kwiatkowska, G. Norman and D. Parker
In P. Kemper, editor, Proc. Tools Session of Aachen 2001 International Multiconference on Measurement, Modelling and Evaluation of Computer-Communication Systems pages 7—12. September 2001.
Available as Technical Report 760/2001, University of Dortmund.
Details
|
BibTeX
| Link (pdf) |
|
[57]
|
Symbolic computation of maximal probabilistic reachability
M. Kwiatkowska, G. Norman and J. Sproston
In K. Larsen, M. Nielsen, editors, Proc. 13th International Conference on Concurrency Theory (CONCUR'01) Vol. 2154 of LNCS, pages 169—183. Springer, 2001.
Details
|
BibTeX
| Link (pdf) |
|
[58]
|
Faster and Symbolic CTMC Model Checking
J.-P. Katoen et al.
In L. de Alfaro, S. Gilmore, editors, Proc. 1st Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM/PROBMIV'01) Vol. 2165 of LNCS, pages 23—38. Springer, September 2001.
Details
|
BibTeX
| Link (pdf) |
|
[59]
|
Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM
M. Kwiatkowska, G. Norman and R. Segala
In G. Berry, H. Comon and A. Finkel, editors, Proc. 13th International Conference on Computer Aided Verification (CAV'01) Vol. 2102 of LNCS, pages 194—206. Springer, July 2001.
Details
|
BibTeX
| Link (pdf) |
|
[60]
|
Verifying Soft Deadlines with Probabilistic Timed Automata
M. Kwiatkowska et al.
In Proc. Workshop on Advances in Verification (Wave'2000) July 2000.
Details
|
BibTeX
| Link (pdf) |
|
[61]
|
Verifying Randomized Distributed Algorithms with PRISM
M. Kwiatkowska, G. Norman and D. Parker
In Proc. Workshop on Advances in Verification (Wave'2000) July 2000.
Details
|
BibTeX
| Link (pdf) |
|
[62]
|
Verifying Quantitative Properties of Continuous Probabilistic Timed Automata
M. Kwiatkowska et al.
In C. Palamidessi, editor, Proc. CONCUR 2000 - Concurrency Theory Vol. 1877 of Lecture Notes in Computer Science, pages 123-137. Springer, 2000.
Details
|
BibTeX
| Link (pdf) |
|
[63]
|
Symbolic Model Checking of Probabilistic Timed Automata Using Backwards Reachability
Marta Z Kwiatkowska, Gethin Norman and Jeremy Sproston
No. CSR-00-01, Technical Report, University of Birmingham, School of Computer Science. January 2000.
Details
|
BibTeX
| Link (pdf) |
|
[64]
|
Symbolic Model Checking of Concurrent Probabilistic Processes Using MTBDDs and the Kronecker Representation
L. de Alfaro et al.
In S. Graf, M. Schwartzbach, editors, Proc. 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'00) Vol. 1785 of LNCS, pages 395—410. Berlin. March 2000. Springer.
Details
|
BibTeX
| Link (pdf) |
|
[65]
|
Symbolic Model Checking of Concurrent Probabilistic Systems Using MTBDDs and Simplex
M. Kwiatkowska et al.
No. CSR-99-1, Technical Report, School of Computer Science, University of Birmingham. January 1999.
Details
|
BibTeX
| Link (pdf) |
|
[66]
|
Solving Infinite Stochastic Process Algebra Models Through Matrix-Geometric Methods
A. El-Rayes, M. Kwiatkowska and G. Norman
In J. Hillston, M. Silva, editors, Proc. 7th Process Algebras and Performance Modelling Workshop (PAPM'99) pages 41—62. University of Zaragoza, 1999.
Details
|
BibTeX
| Link (pdf) |
|
[67]
|
Computing Probability Lower and Upper Bounds for LTL Formulae over Sequential and Concurrent Markov Chains
C. Baier, M. Kwiatkowska and G. Norman
In C. Baier et al. , editors, Proc. 1st Probabilistic Methods in Verification Workshop (PROBMIV'98) Vol. 22 of Electronic Notes in Theoretical Computer Science. Elsevier Science, 1999.
Details
|
BibTeX
| Link (pdf) |
|
[68]
|
Automatic Verification of Real-Time Systems with Discrete Probability Distributions
M. Kwiatkowska et al.
In J.-P. Katoen, editor, Proc. 5th International AMAST Workshop on Real-Time and Probabilistic Systems (ARTS'99) Vol. 1601 of LNCS, pages 75—95. Bamberg. March 1999. Springer.
Details
|
BibTeX
| Link (pdf) |
|
[69]
|
A Testing Equivalence for Reactive Probabilistic Processes
M. Kwiatkowska, G. Norman
In A Testing Equivalence for Reactive Probabilistic Processes Vol. 16(2) of Electronic Notes in Theoretical Computer Science. Elsevier Science, 1998.
Details
|
BibTeX
| Link (pdf) |
|
[70]
|
A Fully Abstract Metric-Space Denotational Semantics for Reactive Probabilistic Processes
M. Kwiatkowska, G. Norman
In Proc. 3rd Workshop on Computation and Approximation (Comprox III) Vol. 13 of Electronic Notes in Theoretical Computer Science. Elsevier Science, 1998.
Details
|
BibTeX
| Link (pdf) |
|
[71]
|
Probabilistic Metric Semantics for a Simple Language with Recursion
M. Kwiatkowska, G. Norman
In W. Penczek, A. Szalas, editors, Proc. 21st International Symposium on Mathematical Foundations of Computer Science (MFCS'96) Vol. 1113 of Lecture Notes in Computer Science, pages 419—430. Springer, 1996.
Details
|
BibTeX
| Link (pdf) |
|
[72]
|
Metric Denotational Semantics for PEPA
M. Kwiatkowska, G. Norman
In M. Ribaudo, editor, Proc. 4th Process Algebras and Performance Modelling Workshop (PAPM'96) pages 120—138. CLUT, 1996.
Details
|
BibTeX
| Link (pdf) |
|
|
|
|
