I am an academic staff member in the
Department of Computer Science, at the
University of Warwick.
My photo and contact details are
here.
Research group
I am a member of the Formal Methods group,
and of DIMAP.
Publications
Logic, automata and games
- M. Jurdzinski, R. Lazic and M. Rutkowski
Average-Price-per-Reward Games on Hybrid Automata with Strong Resets
10th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)
Lecture Notes in Computer Science 5403: 167-181, Springer, January 2009
- P. Bouyer, T. Brihaye, M. Jurdzinski, R. Lazic and M. Rutkowski
Average-price and reachability-price games on hybrid automata with strong resets
6th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS)
Lecture Notes in Computer Science 5215: 63-77, Springer, September 2008
- 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
Extended version: Model checking memoryful linear-time logics over one-counter automata
- 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
Extended version: Alternating automata on data trees and XPath satisfiability
- 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
Extended version: Safety alternating automata on data words
- S. Demri and R. Lazic
LTL with the Freeze Quantifier and Register Automata
Transactions on Computational Logic 10(3), 30 pages, ACM, 2009
arXiv version
- 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
arXiv version
- 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
Infinite-state systems
- S. Demri, M. Jurdzinski, O. Lachish and R. Lazic
The covering and boundedness problems for branching vector addition systems
29th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS): 181-192
LIPIcs, Schloss Dagstuhl, December 2009
- R. Lazic, T. Newcomb, J. Ouaknine, A.W. Roscoe and J. Worrell
Nets with tokens which carry data
Fundamenta Informaticae 88(3): 251-274, 2008
- R. Lazic, T. Newcomb, J. Ouaknine, A.W. Roscoe and J. Worrell
Nets with tokens which carry data
28th International Conference on Application and Theory of Petri Nets and Other Models of Concurrency (ICATPN)
Lecture Notes in Computer Science 4546: 301-320, Springer, June 2007
- 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
Preliminary version
- 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
Software model checking
- 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.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
Full version
- 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
Preliminary version
- 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
Data independence
- 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
Non-well-founded sets
- 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
Editorial work
- R. Lazic and R. Nagarajan (guest editors)
Selected papers arising from AVoCS 2005
Formal Aspects of Computing 19(3), Springer, 2007
- R. Lazic and R. Nagarajan (guest editors)
Proceedings of AVoCS 2005
Electronic Notes in Theoretical Computer Science 145, Elsevier, January 2006
Tools
- GameChecker:
A model checker for open procedural programs based on
game semantics, counter-example guided abstraction refinement, CSP and FDR
PhD students
Biography
I was born (1975) in Belgrade, Serbia, where I attended
Matematicka gimnazija and
Petnica, and was a member of
Arhimedes.
From 1992, I spent 8 years at Oxford University,
obtaining a BA in Mathematics and Computation (1994)
and a DPhil (i.e. PhD) in Computing (1999),
and as a Junior Research Fellow (i.e. postdoc).
During that time, my colleges were
University College,
Merton College and
Christ Church.
Since 2001, I am an academic staff member at
Warwick University.
Curriculum Vitae
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.
Page updated 04/11/2009.