Search

• < Previous
• 1
• Next >

---

Software Model Checking with Explicit Scheduler and Symbolic Threads

Alessandro Cimatti ; Iman Narasamdya ; Marco Roveri.

In many practical application domains, the software is organized into a set of threads, whose activation is exclusive and controlled by a cooperative scheduling policy: threads execute, without any interruption, until they either terminate or yield the control explicitly to the scheduler. The formal&nbsp;[&hellip;]

---

A first-order logic characterization of safety and co-safety languages

Alessandro Cimatti ; Luca Geatti ; Nicola Gigante ; Angelo Montanari ; Stefano Tonetta.

Linear Temporal Logic (LTL) is one of the most popular temporal logics, that comes into play in a variety of branches of computer science. Among the various reasons of its widespread use there are its strong foundational properties: LTL is equivalent to counter-free omega-automata, to star-free&nbsp;[&hellip;]

---