Article by Piterman appears in the JACM

Nir Piterman has had a paper published in the prestigious Journal of the ACM.

The paper "Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems" enables the automated verification of systems with applications to device-drivers and system code. This is achieved by showing how model-checkers can be used to analyse CTL* models (a very expressive temporal logic subsuming both LTL and CTL). This paper demonstrates the viability of the approach in practice, thus leading to a new class of fully automated tools capable of proving crucial properties that no tool could previously prove.

Share this page:

Contact Us

Admissions Enquiries:
BSc: +44 (0) 116 252 5280
MSc: +44 (0) 116 252 2265
E: BSc
E: MSc

Departmental Enquiries:
T: +44 (0) 116 252 2129/3887
F: +44 (0) 116 252 3604

Dept of Informatics
University of Leicester
Leicester, LE1 7RH
United Kingdom


AccessAble logo

The University of Leicester is committed to equal access to our facilities. DisabledGo has a detailed accessibility guide for the Informatics Building.