Project Publications
Sort by: date, type, title
15 publications:
-
[KNS01a]
M. Kwiatkowska, G. Norman and R. Segala.
Automated Verification of a Randomised Distributed Consensus Protocol Using Cadence SMV and PRISM.
In G. Berry, H. Common and A. Finkel (editors), Proc. CAV'01, volume 2102 of Lecture Notes in Computer Science, pages 194-206, Springer.
January 2001.
[ps.gz]
[pdf]
[bib]
-
[KNSS02]
M. Kwiatkowska, G. Norman, R. Segala and J. Sproston.
Automatic Verification of Real-time Systems with Discrete Probability Distributions.
Theoretical Computer Science, 282, pages 101-150.
June 2002.
[ps.gz]
[pdf]
[bib]
-
[KNSS99]
M. Kwiatkowska, G. Norman, R. Segala and J. Sproston.
Automatic Verification of Real-Time Systems with Discrete Probability Distributions.
In J.-P. Katoen (editor), Proc. 5th International AMAST Workshop on Real-Time and Probabilistic Systems (ARTS'99), volume 1601 of LNCS, pages 75--95, Springer.
March 1999.
[ps.gz]
[pdf]
[bib]
-
[BKN99]
C. Baier, M. Kwiatkowska and G. Norman.
Computing Probability Lower and Upper Bounds for LTL Formulae over Sequential and Concurrent Markov Chains.
In C. Baier and M. Huth and M. Kwiatkowska and M. Ryan (editors), Proc. 1st Probabilistic Methods in Verification Workshop (PROBMIV'98), volume 22 of Electronic Notes in Theoretical Computer Science, Elsevier Science.
June 1999.
[ps.gz]
[pdf]
[bib]
-
[KKNP01]
J.-P. Katoen, M. Kwiatkowska, G. Norman and D. Parker.
Faster and Symbolic CTMC Model Checking.
In L. de Alfaro and S. Gilmore (editors), Proc. PAPM/PROBMIV'01, volume 2165 of Lecture Notes in Computer Science, pages 23-38, Springer.
September 2001.
[ps.gz]
[pdf]
[bib]
-
[HKN+03]
H. Hermanns, M. Kwiatkowska, G. Norman, D. Parker and M. Siegle.
On the use of MTBDDs for Performability Analysis and Verification of Stochastic Systems.
Journal of Logic and Algebraic Programming: Special Issue on Probabilistic Techniques for the Design and Analysis of Systems, 56, pages 23-67, Elsevier.
June 2003.
[ps.gz]
[pdf]
[bib]
-
[KNP02a]
M. Kwiatkowska, G. Norman and D. Parker.
PRISM: Probabilistic Symbolic Model Checker.
In T. Field, P. Harrison, J. Bradley and U. Harder (editors), Proc. TOOLS 2002, volume 2324 of Lecture Notes in Computer Science, pages 200-204, Springer.
April 2002.
[ps.gz]
[pdf]
[bib]
-
[KNS03b]
M. Kwiatkowska, G. Norman and J. Sproston.
Probabilistic Model Checking of Deadline Properties in the IEEE1394 FireWire Root Contention Protocol.
Formal Aspects of Computing, 14(3), pages 295-318.
April 2003.
[ps.gz]
[pdf]
[bib]
-
[KNP02b]
M. Kwiatkowska, G. Norman and D. Parker.
Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach.
In J-P. Katoen and P. Stevens (editors), Proc. TACAS'02, volume 2280 of Lecture Notes in Computer Science, pages 52-66, Springer.
April 2002.
[ps.gz]
[pdf]
[bib]
-
[EKN99]
A. El-Rayes, M. Kwiatkowska and G. Norman.
Solving Infinite Stochastic Process Algebra Models Through Matrix-Geometric Methods.
In J. Hillston and M. Silva (editors), Proc. 7th Process Algebras and Performance Modelling Workshop (PAPM'99), pages 41-62, University of Zaragoza.
September 1999.
[ps.gz]
[pdf]
[bib]
-
[KNS01b]
M. Kwiatkowska, G. Norman and J. Sproston.
Symbolic computation of maximal probabilistic reachability.
In K. Larsen and M. Nielsen (editors), Proc. 13th International Conference on Concurrency Theory (CONCUR'01), volume 2154 of LNCS, pages 169--183, Springer.
August 2001.
[ps.gz]
[pdf]
[bib]
-
[dAKN+00]
L. de Alfaro, M. Kwiatkowska, G. Norman, D. Parker and R. Segala.
Symbolic Model Checking of Probabilistic Processes using MTBDDs and the Kronecker Representation.
In S. Graf and M. Schwartzbach (editors), Proc. TACAS'00, volume 1785 of Lecture Notes in Computer Science, pages 395-410, Springer.
March 2000.
[ps.gz]
[pdf]
[bib]
-
[KNS00]
M. Kwiatkowska, G. Norman and J. Sproston.
Symbolic Model Checking of Probabilistic Timed Automata Using Backwards Reachability.
Technical report CSR-00-01, University of Birmingham, School of Computer Science.
January 2000.
[ps.gz]
[pdf]
[bib]
-
[KNSS00a]
M. Kwiatkowska, G. Norman, R. Segala and J. Sproston.
Verifying Quantitative Properties of Continuous Probabilistic Timed Automata.
In C. Palamidessi (editor), Proc. CONCUR 2000 - Concurrency Theory, volume 1877 of Lecture Notes in Computer Science, pages 123-137, Springer.
August 2000.
[ps.gz]
[pdf]
[bib]
-
[KN02]
M. Kwiatkowska and G. Norman.
Verifying Randomized Byzantine Agreement.
In D. Peled and M. Vardi (editors), Proc. Formal Techniques for Networked and Distributed Systems (FORTE'02), volume 2529 of Lecture Notes in Computer Science, pages 194-209, Springer.
November 2002.
[ps.gz]
[pdf]
[bib]
Sort by: date, type, title
