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: