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.