Publications

2012
J. Markovski, “Process theory for supervisory control of stochastic systems with data”, in ETFA, 2012.
J. Markovski, “Process theory for supervisory control with partial observation of events and states”, in CDC, 2012.
J. Markovski, “A process-theoretic state-based framework for live supervision”, in CASE, 2012.
M. S. Alvim, M. E. Andrés, and C. Palamidessi, “Quantitative information flow in interactive systems”, Journal of Computer Security, vol. 20, p. 3-50, 2012.PDF iconfull.pdf (532.59 KB)
Quantitative Security Analysis (Dagstuhl Seminar 12481)”, Dagstuhl Reports, vol. 2. p. 135-154, 2012.
D. Guck, T. Han, J. - P. Katoen, and M. R. Neuhäußer, “Quantitative Timed Analysis of Interactive Markov Chains”, in 4th International Symposium NASA Formal Methods (NFM), Norfolk, USA, 2012, vol. 7226, p. 8-23.PDF icon72260008.pdf (256.53 KB)
J. Markovski, P. R. D'Argenio, J. C. M. Baeten, and E. P. de Vink, “Reconciling real and stochastic time: the need for probabilistic refinement”, Formal Aspects of Computing, vol. 24, p. 497-518, 2012.
C. G. López Pombo, P. F. Castro, N. Aguirre, and T. S. E. Maibaum, “Satisfiability Calculus: The Semantic Counterpart of a Proof Calculus in General Logics”, in Recent Trends in Algebraic Development Techniques, 21st International Workshop, {WADT} 2012, Salamanca, Spain, June 7-10, 2012, Revised Selected Papers, 2012.
J. Bogdoll, A. Hartmanns, and H. Hermanns, “Simulation and Statistical Model Checking for Modestly Nondeterministic Models”, in Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance, 2012, vol. 7201, p. 249-252.
D. Déharbe, P. Fontaine, Y. Guyot, and L. Voisin, “SMT Solvers for Rodin”, in 3rd Intl. Conf. Abstract State Machines, Alloy, B, VDM, and Z (ABZ 2012), Pisa, Italy, 2012.
S. Knight, C. Palamidessi, P. Panangaden, and D. Valencia, Frank, “Spatial and Epistemic Modalities in Constraint-Based Process Calculi”, in Proceedings of CONCUR, Newcastle upon Tyne, UK, 2012.PDF iconhal.archives-ouvertes.fr:docs:00:76:11:16:PDF:eccp.pdf (2.71 MB)
S. Abramsky, M. W. Mislove, and C. Palamidessi, “Special issue dedicated to a selection of papers of the conference Mathematical Foundations of Programming Semantics (MFPS XXV)”, Theor. Comput. Sci., vol. 430, p. 1-2, 2012.
G. Regis, N. Ricci, N. Aguirre, and T. S. E. Maibaum, “Specifying and Verifying Declarative Fluent Temporal Logic Properties of Workflows”, in Formal Methods: Foundations and Applications - 15th Brazilian Symposium, {SBMF} 2012, Natal, Brazil, September 23-28, 2012. Proceedings, 2012.PDF iconWorkflowPropVerification.pdf (433.21 KB)
M. Bozga, et al., “State-of-the-art tools and techniques for quantitative modeling and analysis of embedded systems”, in 2012 Design, Automation {&} Test in Europe Conference {&} Exhibition, DATE 2012, Dresden, Germany, March 12-16, 2012, 2012.
R. Bruni, H. C. Melgratti, and U. Montanari, “A survey on basic connectors and buffers”, in Formal Methods for Components and Objects - 10th International Symposium, FMCO 2011. Revised Papers, 2012.
C. Areces, G. Hoffmann, and E. Orbe, “Symmetries in Modal Logics: A Coinductive Approach”, in Proceedings of the 7th Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2012), Rio de Janeiro, 2012.
R. Corin and F. Manzano, “Taint Analysis of Security Code in the KLEE Symbolic Execution Engine”, in 2012 International Conference on Information and Communications Security (ICICS), Hong Kong, 2012.PDF icon76180264 (1).pdf (252.37 KB)
D. Cousineau, D. Doligez, L. Lamport, S. Merz, D. Ricketts, and H. Vanzetto, “TLA+ Proofs”, in 18th Intl. Symp. Formal Methods (FM 2012), Paris, France, 2012.
M. D. Lee, D. Gebler, and P. R. D'Argenio, “Tree rules in probabilistic transition system specifications with negative and quantitative premises”, Electronic Proceedings in Theoretical Computer Science, vol. 89, p. 115 - 130, 2012.
F. Arnold, D. Gebler, D. Guck, and H. Hatefi, “A Tutorial on Interactive Markov Chains”, in {ROCKS}, 2012.
V. S. Bengolea, N. Aguirre, D. Marinov, and M. F. Frias, “Using Coverage Criteria on RepOK to Reduce Bounded Exhaustive Test Suites”, in International Conference on Tests and Proofs TAP 2012, vol. 7305, 2012, p. 19 - 34.PDF icontestsuite-reduction.pdf (262.31 KB)
L. M. Ferrer Fioriti, E. M. Hahn, H. Hermanns, and B. Wachter, “Variable Probabilistic Abstraction Refinement”, in Automated Technology for Verification and Analysis - 10th International Symposium, ATVA 2012, Thiruvananthapuram, India, October 3-6, 2012. Proceedings, 2012, vol. 7561, p. 300-316.
T. Brázdil, H. Hermanns, J. Krčál, J. Kret\'ınský, and V. Rehák, “Verification of Open Interactive Markov Chains”, in IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2012, December 15-17, 2012, Hyderabad, India, 2012.
E. E. S. Musa, “Verification of Stochastic Requirements in Supervised Plants”, SE Report, TUE. 2012.
K. Bhargavan, C. Fournet, R. Corin, and E. Zalinescu, “Verified Cryptographic Implementations for TLS”, ACM Trans. Inf. Syst. Secur., vol. 15, p. 3, 2012.

Pages