Skip to main content

Selected Publications

Energy, parity and related games

Petri nets and related models

Data logics and automata

  • S. Demri, R. Lazic and A. Sangnier
    Model checking memoryful linear-time logics over one-counter automata
    Theoretical Computer Science 411(22-24): 2298-2316, 2010
  • S. Demri, R. Lazic and A. Sangnier
    Model checking freeze LTL over one-counter automata
    11th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS)
    Lecture Notes in Computer Science 4962: 490-504, Springer, March 2008
  • M. Jurdzinski and R. Lazic
    Alternating automata on data trees and XPath satisfiability
    Transactions on Computational Logic 12(3), 23 pages, ACM, 2011
  • M. Jurdzinski and R. Lazic
    Alternation-free modal mu-calculus for data trees
    22nd Annual Symposium on Logic in Computer Science (LICS): 131-140
    IEEE, July 2007
  • R. Lazic
    Safety alternating automata on data words
    Transactions on Computational Logic 12(2), 23 pages, ACM, 2011
  • R. Lazic
    Safely Freezing LTL
    26th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)
    Lecture Notes in Computer Science 4337: 381-392, Springer, December 2006
  • S. Demri and R. Lazic
    LTL with the Freeze Quantifier and Register Automata
    Transactions on Computational Logic 10(3), 30 pages, ACM, 2009
  • S. Demri and R. Lazic
    LTL with the Freeze Quantifier and Register Automata
    21st Annual Symposium on Logic in Computer Science (LICS): 17-26 Talk
    IEEE, August 2006
  • S. Demri, R. Lazic and D. Nowak
    On the freeze quantifier in constraint LTL: decidability and complexity
    Information and Computation 205(1): 2-24, Elsevier, 2007
  • S. Demri, R. Lazic and D. Nowak
    On the freeze quantifier in constraint LTL: decidability and complexity
    12th International Symposium on Temporal Representation and Reasoning (time): 113-121
    IEEE, June 2005

Verification and game semantics

  • R. Lazic and A.S. Murawski
    Contextual approximation and higher-order procedures
    19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS)
    Lecture Notes in Computer Science 9634: 162-179, Springer, April 2016
  • A.S. Dimovski and R. Lazic
    Assume-Guarantee Software Verification Based on Game Semantics
    8th International Conference on Formal Engineering Methods (ICFEM)
    Lecture Notes in Computer Science 4260: 529-548, Springer, November 2006
    Overview talk given at GaLoP '06
  • A. Bakewell, A. Dimovski, D.R. Ghica and R. Lazic
    Data-Abstraction Refinement: A Game Semantic Approach
    International Journal on Software Tools for Technology Transfer (STTT) 12(5): 373-389, Springer, 2010
    Supercedes the SAS '05 and SPIN '06 papers
  • A.S. Dimovski, D.R. Ghica and R. Lazic
    A Counterexample-Guided Refinement Tool for Open Procedural Programs
    13th International SPIN Workshop on Model Checking of Software (SPIN)
    Lecture Notes in Computer Science 3925: 288-292, Springer, March 2006
  • A.S. Dimovski, D.R. Ghica and R. Lazic
    Data-Abstraction Refinement: A Game Semantic Approach
    12th International Static Analysis Symposium (SAS)
    Lecture Notes in Computer Science 3672: 102-117, Springer, September 2005
  • A.S. Dimovski and R. Lazic
    Compositional Software Verification Based on Game Semantics and Process Algebra
    International Journal on Software Tools for Technology Transfer (STTT) 9(1): 37-51, Springer, 2007
    Supercedes the AVoCS '04 and ICFEM '04 papers
  • A.S. Dimovski and R. Lazic
    Software Model Checking Based on Game Semantics and CSP
    4th International Workshop on Automated Verification of Critical Systems (AVoCS '04)
    Electronic Notes in Theoretical Computer Science 128(6): 105-125, Elsevier, May 2005
  • A.S. Dimovski and R. Lazic
    CSP Representation of Game Semantics for Second-order Idealized Algol
    6th International Conference on Formal Engineering Methods (ICFEM)
    Lecture Notes in Computer Science 3308: 146-161, Springer, November 2004

Timed and hybrid systems

Polymorphic systems with arrays

  • R. Lazic
    Decidability of Reachability for Polymorphic Systems with Arrays: A Complete Classification
    6th International Workshop on Verification of Infinite-State Systems (Infinity '04)
    Electronic Notes in Theoretical Computer Science 138(3): 3-19, Elsevier, December 2005
  • R. Lazic, T. Newcomb and A.W. Roscoe
    Polymorphic Systems with Arrays, 2-Counter Machines and Multiset Rewriting
    6th International Workshop on Verification of Infinite-State Systems (Infinity '04)
    Electronic Notes in Theoretical Computer Science 138(3): 61-86, Elsevier, December 2005
    Research report version: CS-RR-399 Talk
  • R. Lazic, T. Newcomb and A.W. Roscoe
    On model checking data-independent systems with arrays with whole-array operations
    Communicating Sequential Processes: The First 25 Years
    Lecture Notes in Computer Science 3525: 275-291, Springer, July 2004
    Research report version: CS-RR-395
  • R.S. Lazic, T.C. Newcomb and A.W. Roscoe
    On model checking data-independent systems with arrays without reset
    Theory and Practice of Logic Programming (TPLP) 4 (5 & 6): 659-693, Cambridge University Press, 2004
    Research report version: RR-02-02
  • A.W. Roscoe and R.S. Lazic
    What can you decide about resetable arrays?
    2nd International Workshop on Verification and Computational Logic (VCL)
    Technical Report DSSE-TR-2001-3: 5-23, September 2001
  • R. Lazic and A.W. Roscoe
    Verifying determinism of concurrent systems which use unbounded arrays
    3rd International Workshop on Verification of Infinite State Systems (INFINITY '98)
    Report TUM-I9825: 2-8, Technical University of Munich, July 1998
    Research report version: PRG-TR-2-98

Verification and process algebra

  • X. Wang, A.W. Roscoe and R.S. Lazic
    Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption
    4th International Conference on Integrated Formal Methods (IFM)
    Lecture Notes in Computer Science 2999: 247-266, Springer, April 2004
    Research report version: RR-03-08
  • R. Lazic and D. Nowak
    On a Semantic Definition of Data Independence
    6th International Conference on Typed Lambda Calculi and Applications (TLCA)
    Lecture Notes in Computer Science 2701: 226-240, Springer, June 2003
    Research report version: CS-RR-392
  • R. Lazic and D. Nowak
    A unifying approach to data-independence
    11th International Conference on Concurrency Theory (CONCUR)
    Lecture Notes in Computer Science 1877: 581-595, Springer, August 2000
    Research report version: PRG-TR-4-00
  • R. Lazic and A.W. Roscoe
    Data independence with generalised predicate symbols
    International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA)
    Volume I: 319-325, CSREA Press, June 1999
  • R.S. Lazic
    A Semantic Study of Data Independence with Applications to Model Checking
    DPhil thesis, Oxford University Computing Laboratory, April 1999

Set theory

  • R.S. Lazic and A.W. Roscoe
    On transition systems and non-well-founded sets
    Papers on General Topology and Applications: 11th Summer Conference at the University of Southern Maine (August 1995)
    Annals of the New York Academy of Sciences 806: 238-264, December 1996

Copyright note: The documents contained in these directories are included by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit written permission of the copyright holder.