Coronavirus (Covid-19): Latest updates and information
Skip to main content Skip to navigation

Formal Methods selected publications

For more publications (including those from before 2001), downloads of publications, and software developed by us, please see the members' pages.

[1]
Stéphane Demri and Ranko Lazic. Ltl with the freeze quantifier and register automata. ACM Trans. Comput. Log., 10(3), 2009.
[2]
Marcin Jurdzinski. Algorithms for solving infinite games. In SOFSEM, pages 46–48, 2009.
[3]
Marcin Jurdzinski, Ranko Lazic, and Michal Rutkowski. Average-price-per-reward games on hybrid automata with strong resets. In VMCAI, pages 167–181, 2009.
[4]
Patricia Bouyer, Thomas Brihaye, Marcin Jurdzinski, Ranko Lazic, and Michal Rutkowski. Average-price and reachability-price games on hybrid automata with strong resets. In FORMATS, pages 63–77, 2008.
[5]
Stéphane Demri, Ranko Lazic, and Arnaud Sangnier. Model checking freeze ltl over one-counter automata. In FoSSaCS, pages 490–504, 2008.
[6]
Marcin Jurdzinski and Rahul Savani. A simple p-matrix linear complementarity problem for discounted games. In CiE, pages 283–293, 2008.
[7]
Marcin Jurdzinski and Ashutosh Trivedi. Average-time games. In FSTTCS, 2008.
[8]
Marcin Jurdzinski and Ashutosh Trivedi. Concavely-priced timed automata. In FORMATS, pages 48–62, 2008.
[9]
Marcin Jurdzinski, Mike Paterson, and Uri Zwick. A deterministic subexponential algorithm for solving parity games. SIAM J. Comput., 38(4):1519–1532, 2008.
[10]
Ranko Lazic, Tom Newcomb, Joël Ouaknine, A. W. Roscoe, and James Worrell. Nets with tokens which carry data. Fundam. Inform., 88(3):251–274, 2008.
[11]
Stéphane Demri, Ranko Lazic, and David Nowak. On the freeze quantifier in constraint LTL: Decidability and complexity. Inf. Comput., 205(1):2–24, 2007.
[12]
Aleksandar Dimovski and Ranko Lazic. Compositional software verification based on game semantics and process algebra. STTT, 9(1):37–51, 2007.
[13]
Marcin Jurdzinski and Ranko Lazic. Alternation-free modal mu-calculus for data trees. In LICS, pages 131–140, 2007.
[14]
Marcin Jurdzinski and Ashutosh Trivedi. Reachability-time games on timed automata. In ICALP, volume 4596, pages 838–849. Springer, 2007.
[15]
Marcin Jurdzinski, François Laroussinie, and Jeremy Sproston. Model checking probabilistic timed automata with one or two clocks. In TACAS, volume 4424 of LNCS, pages 170–184. Springer, 2007.
[16]
Ranko Lazic and Rajagopal Nagarajan. Guest editorial. Formal Asp. Comput., 19(3):275, 2007.
[17]
Ranko Lazic, Thomas Christopher Newcomb, Joël Ouaknine, A. W. Roscoe, and James Worrell. Nets with tokens which carry data. In ICATPN, pages 301–320, 2007.
[18]
Krishnendu Chatterjee, Thomas A. Henzinger, and Marcin Jurdzinski. Games with secure equilibria. Theor. Comput. Sci., 365(1-2):67–82, 2006.
[19]
Stéphane Demri and Ranko Lazic. LTL with the freeze quantifier and register automata. In LICS, pages 17–26, 2006.
[20]
Aleksandar Dimovski and Ranko Lazic. Assume-guarantee software verification based on game semantics. In ICFEM, pages 529–548, 2006.
[21]
Aleksandar Dimovski, Dan R. Ghica, and Ranko Lazic. A counterexample-guided refinement tool for open procedural programs. In SPIN, pages 288–292, 2006.
[22]
Simon Hammond and David Lacey. Loop transformations in the ahead-of-time optimization of Java bytecode. In CC, pages 109–123, 2006.
[23]
Marcin Jurdzinski, Mike Paterson, and Uri Zwick. A deterministic subexponential algorithm for solving parity games. In SODA, pages 117–123, 2006.
[24]
Ranko Lazic. Safely freezing LTL. In FSTTCS, pages 381–392, 2006.
[25]
Ranko Lazic and Rajagopal Nagarajan. Preface. Electr. Notes Theor. Comput. Sci., 145:1–2, 2006.
[26]
Peter Niebert and Doron Peled. Efficient model checking for LTL with partial order snapshots. In TACAS, pages 272–286, 2006.
[27]
Doron Peled and Hongyang Qu. Enforcing concurrent temporal behaviors. Int. J. Found. Comput. Sci., 17(4):743–762, 2006.
[28]
Rajeev Alur, Kenneth L. McMillan, and Doron Peled. Deciding global partial-order properties. Formal Methods in System Design, 26(1):7–25, 2005.
[29]
Saddek Bensalem, Doron Peled, Hongyang Qu, and Stavros Tripakis. Generating path conditions for timed systems. In IFM, pages 5–19, 2005.
[30]
Garry Bowen and Rajagopal Nagarajan. On feedback and the classical capacity of a noisy quantum channel. IEEE Transactions on Information Theory, 51(1):320–324, 2005.
[31]
Krishnendu Chatterjee, Thomas A. Henzinger, and Marcin Jurdzinski. Mean-payoff parity games. In LICS, pages 178–187, 2005.
[32]
Chien-An Chen, Sara Kalvala, and Jane Sinclair. A process-based semantics for Message Sequence Charts with data. In Australian Software Engineering Conference, pages 130–139, 2005.
[33]
Chien-An Chen, Sara Kalvala, and Jane Sinclair. Race conditions in Message Sequence Charts. In APLAS, pages 195–211, 2005.
[34]
Stéphane Demri, Ranko Lazic, and David Nowak. On the freeze quantifier in constraint LTL: Decidability and complexity. In TIME, pages 113–121, 2005.
[35]
Aleksandar Dimovski and Ranko Lazic. Software model checking based on game semantics and CSP. Electr. Notes Theor. Comput. Sci., 128(6):105–125, 2005.
[36]
Aleksandar Dimovski, Dan R. Ghica, and Ranko Lazic. Data-abstraction refinement: A game semantic approach. In SAS, pages 102–117, 2005.
[37]
Simon J. Gay and Rajagopal Nagarajan. Communicating quantum processes. In POPL, pages 145–157, 2005.
[38]
Blaise Genest, Dietrich Kuske, Anca Muscholl, and Doron Peled. Snapshot verification. In TACAS, pages 510–525, 2005.
[39]
Elsa L. Gunter and Doron Peled. Model checking, testing and verification working together. Formal Asp. Comput., 17(2):201–221, 2005.
[40]
Arshad Jhumka and Martin Hiller. Putting detectors in their place. In SEFM, pages 33–43, 2005.
[41]
Arshad Jhumka and Neeraj Suri. Designing efficient fail-safe multitolerant systems. In FORTE, pages 428–442, 2005.
[42]
Arshad Jhumka, Stephan Klaus, and Sorin A. Huss. A dependability-driven system-level design approach for embedded systems. In DATE, pages 372–377, 2005.
[43]
Marcin Jurdzinski, Doron Peled, and Hongyang Qu. Calculating probabilities of real-time test cases. In FATES, pages 134–151, 2005.
[44]
Ralph Kopperman, Steve Matthews, and Homeira Pajoohesh. What do partial metrics represent? In Spatial Representation, 2005.
[45]
Ranko Lazic. Decidability of reachability for polymorphic systems with arrays: A complete classification. Electr. Notes Theor. Comput. Sci., 138(3):3–19, 2005.
[46]
Ranko Lazic, Thomas Christopher Newcomb, and Bill Roscoe. Polymorphic systems with arrays, 2-counter machines and multiset rewriting. Electr. Notes Theor. Comput. Sci., 138(3):61–86, 2005.
[47]
Doron Peled. Introduction: Special issue on partial order in formal methods. Formal Methods in System Design, 26(1):5–6, 2005.
[48]
Doron Peled and Hongyang Qu. Enforcing concurrent temporal behaviors. Electr. Notes Theor. Comput. Sci., 113:65–83, 2005.
[49]
Doron Peled and Hongyang Qu. Time unbalanced partial order. In FATES, pages 152–169, 2005.
[50]
Doron Peled and Yih-Kuen Tsay, editors. Automated Technology for Verification and Analysis, Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005, Proceedings, volume 3707 of Lecture Notes in Computer Science. Springer, 2005.
[51]
Rajeev Alur and Doron Peled, editors. Computer Aided Verification, 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings, volume 3114 of Lecture Notes in Computer Science. Springer, 2004.
[52]
Krishnendu Chatterjee, Thomas A. Henzinger, and Marcin Jurdzinski. Games with secure equilibria. In LICS, pages 160–169, 2004.
[53]
Krishnendu Chatterjee, Marcin Jurdzinski, and Thomas A. Henzinger. Quantitative stochastic parity games. In SODA, pages 121–130, 2004.
[54]
Krishnendu Chatterjee, Rupak Majumdar, and Marcin Jurdzinski. On Nash equilibria in stochastic games. In CSL, pages 26–40, 2004.
[55]
Aleksandar Dimovski and Ranko Lazic. CSP representation of game semantics for second-order Idealized Algol. In ICFEM, pages 146–161, 2004.
[56]
Felix C. Gärtner and Arshad Jhumka. Automating the addition of fail-safe fault-tolerance: Beyond fusion-closed specifications. In FORMATS/FTRTFT, pages 183–198, 2004.
[57]
Blaise Genest, Marius Minea, Anca Muscholl, and Doron Peled. Specifying and verifying partial order properties using Template MSCs. In FoSSaCS, pages 195–210, 2004.
[58]
Martin Hiller, Arshad Jhumka, and Neeraj Suri. EPIC: Profiling the propagation and effect of data errors in software. IEEE Trans. Computers, 53(5):512–530, 2004.
[59]
Arshad Jhumka, Martin Hiller, and Neeraj Suri. An approach for designing and assessing detectors for dependable component-based systems. In HASE, pages 69–78, 2004.
[60]
Andréas Johansson, Adina Sarbu, Arshad Jhumka, and Neeraj Suri. On enhancing the robustness of commercial operating systems. In ISAS, pages 148–159, 2004.
[61]
Ralph Kopperman, Steve Matthews, and Homeira Pajoohesh. Philosophical issues in computer science. In WSPI, 2004.
[62]
David Lacey, Neil D. Jones, Eric Van Wyk, and Carl Christian Frederiksen. Compiler optimization correctness by temporal logic. Higher-Order and Symbolic Computation, 17(3):173–206, 2004.
[63]
Ranko Lazic, Thomas Christopher Newcomb, and A. W. Roscoe. On model checking data-independent systems with arrays with whole-array operations. In 25 Years Communicating Sequential Processes, pages 275–291, 2004.
[64]
Ranko Lazic, Thomas Christopher Newcomb, and A. W. Roscoe. On model checking data-independent systems with arrays without reset. TPLP, 4(5-6):659–693, 2004.
[65]
Xu Wang, A. W. Roscoe, and Ranko Lazic. Relating data independent trace checks in CSP with UNITY reachability under a normality assumption. In IFM, pages 247–266, 2004.
[66]
Krishnendu Chatterjee, Marcin Jurdzinski, and Thomas A. Henzinger. Simple stochastic parity games. In CSL, pages 100–113, 2003.
[67]
Michael F. Cowlishaw. Decimal floating-point: Algorism for computers. In IEEE Symposium on Computer Arithmetic, pages 104–111, 2003.
[68]
Oege de Moor, David Lacey, and Eric Van Wyk. Universal regular path queries. Higher-Order and Symbolic Computation, 16(1-2):15–35, 2003.
[69]
Berndt Farwer, Saraswati Kalvala, and Kundan Misra. Controller synthesis for Object Petri nets. In ICFEM, pages 432–451, 2003.
[70]
Simon J. Gay and Rajagopal Nagarajan. Intensional and extensional semantics of dataflow programs. Formal Asp. Comput., 15(4):299–318, 2003.
[71]
Blaise Genest, Anca Muscholl, and Doron Peled. Message Sequence Charts. In Lectures on Concurrency and Petri Nets, pages 537–558, 2003.
[72]
Elsa L. Gunter and Doron Peled. Unit checking: Symbolic model checking for a unit of code. In Verification: Theory and Practice, pages 548–567, 2003.
[73]
Elsa L. Gunter, Anca Muscholl, and Doron Peled. Compositional Message Sequence Charts. STTT, 5(1):78–89, 2003.
[74]
Arshad Jhumka, Neeraj Suri, and Martin Hiller. A framework for the design and validation of efficient fail-safe fault-tolerant programs. In SCOPES, pages 182–197, 2003.
[75]
Marcin Jurdzinski, Mogens Nielsen, and Jirí Srba. Undecidability of domino games and hhp-bisimilarity. Inf. Comput., 184(2):343–368, 2003.
[76]
Ranko Lazic and David Nowak. On a semantic definition of data independence. In TLCA, pages 226–240, 2003.
[77]
Anca Muscholl and Doron Peled. Deciding properties of Message Sequence Charts. In Scenarios: Models, Transformations and Tools, pages 43–65, 2003.
[78]
Doron Peled. Model checking and testing combined. In ICALP, pages 47–63, 2003.
[79]
Doron Peled and Hongyang Qu. Automatic verification of annotated code. In FORTE, pages 127–143, 2003.
[80]
Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, Marcin Jurdzinski, and Freddy Y. C. Mang. Interface compatibility checking for software modules. In CAV, pages 428–441, 2002.
[81]
Cindy Eisner and Doron Peled. Comparing symbolic and explicit model checking of a software system. In SPIN, pages 230–239, 2002.
[82]
Alex Groce, Doron Peled, and Mihalis Yannakakis. Adaptive model checking. In TACAS, pages 357–370, 2002.
[83]
Alex Groce, Doron Peled, and Mihalis Yannakakis. AMC: An adaptive model checker. In CAV, pages 521–525, 2002.
[84]
Elsa L. Gunter and Doron Peled. Temporal debugging for concurrent systems. In TACAS, pages 431–444, 2002.
[85]
Elsa L. Gunter and Doron Peled. Tracing the executions of concurrent programs. Electr. Notes Theor. Comput. Sci., 70(4), 2002.
[86]
Chris Hankin, Rajagopal Nagarajan, and Prahladavaradan Sampath. Flow analysis: Games and nets. In The Essence of Computation, pages 135–156, 2002.
[87]
Martin Hiller, Arshad Jhumka, and Neeraj Suri. On the placement of software mechanisms for detection of data errors. In DSN, pages 135–144, 2002.
[88]
Martin Hiller, Arshad Jhumka, and Neeraj Suri. PROPANE: an environment for examining the propagation of errors in software. In ISSTA, pages 81–85, 2002.
[89]
Arshad Jhumka, Martin Hiller, Vilgot Claesson, and Neeraj Suri. On systematic design of globally consistent executable assertions in embedded software. In LCTES-SCOPES, pages 75–84, 2002.
[90]
Arshad Jhumka, Martin Hiller, and Neeraj Suri. An approach to specify and test component-based dependable software. In HASE, pages 211–220, 2002.
[91]
Arshad Jhumka, Martin Hiller, and Neeraj Suri. Component-based synthesis of dependable embedded software. In FTRTFT, pages 111–128, 2002.
[92]
Marcin Jurdzinski, Orna Kupferman, and Thomas A. Henzinger. Trading probability for fairness. In CSL, pages 292–305, 2002.
[93]
Robert P. Kurshan, Vladimir Levin, Marius Minea, Doron Peled, and Hüsnü Yenigün. Combining software and hardware verification techniques. Formal Methods in System Design, 21(3):251–280, 2002.
[94]
David Lacey, Neil D. Jones, Eric Van Wyk, and Carl Christian Frederiksen. Proving correctness of compiler optimizations by temporal logic. In POPL, pages 283–294, 2002.
[95]
Doron Peled. Specification and verification using Message Sequence Charts. Electr. Notes Theor. Comput. Sci., 65(7), 2002.
[96]
Doron Peled and Moshe Y. Vardi, editors. Formal Techniques for Networked and Distributed Systems - FORTE 2002, 22nd IFIP WG 6.1 International Conference Houston, Texas, USA, November 11-14, 2002, Proceedings, volume 2529 of Lecture Notes in Computer Science. Springer, 2002.
[97]
Doron Peled, Moshe Y. Vardi, and Mihalis Yannakakis. Black box checking. Journal of Automata, Languages and Combinatorics, 7(2):225–246, 2002.
[98]
Rajeev Alur, Kousha Etessami, Salvatore La Torre, and Doron Peled. Parametric temporal logic for "model measuring". ACM Trans. Comput. Log., 2(3):388–407, 2001.
[99]
Michael F. Cowlishaw, Eric M. Schwarz, Ronald M. Smith, and Charles F. Webb. A decimal floating-point specification. In IEEE Symposium on Computer Arithmetic, pages 147–154, 2001.
[100]
Elsa L. Gunter, Anca Muscholl, and Doron Peled. Compositional Message Sequence Charts. In TACAS, pages 496–511, 2001.
[101]
Martin Hiller, Arshad Jhumka, and Neeraj Suri. An approach for analysing the propagation of data errors in software. In DSN, pages 161–172, 2001.
[102]
Arshad Jhumka, Martin Hiller, and Neeraj Suri. Assessing inter-modular error propagation in distributed software. In SRDS, pages 152–161, 2001.
[103]
David Lacey and Oege de Moor. Imperative program transformation by rewriting. In CC, pages 52–68, 2001.
[104]
Anca Muscholl and Doron Peled. From finite state communication protocols to high-level Message Sequence Charts. In ICALP, pages 720–731, 2001.
[105]
Doron Peled and Lenore D. Zuck. From model checking to a temporal proof. In SPIN, pages 1–14, 2001.
[106]
Doron Peled, Amir Pnueli, and Lenore D. Zuck. From falsification to verification. In FSTTCS, pages 292–304, 2001.
[107]
Doron Peled, Antti Valmari, and Ilkka Kokkarinen. Relaxed visibility enhances partial order reduction. Formal Methods in System Design, 19(3):275–289, 2001.
[108]
Natasha Sharygina and Doron Peled. A combined testing and verification approach for software reliability. In FME, pages 611–628, 2001.

This bibliography was generated using bib2xhtml.