Program verification aims at ensuring a program satisfies a given desirable property. Temporal logics form an important class of specification languages. Advances in dealing with existential temporal properties of programs are not on par with that of universal properties. We propose a Horn constraints based method that can not only formalize declaratively but also solve efficiently various problems in formal methods that involve existential (and universal) temporal properties. We apply our method to verify branching-time temporal properties and compute winning strategies in graph games over infinite-state programs.      «

Program verification aims at ensuring a program satisfies a given desirable property. Temporal logics form an important class of specification languages. Advances in dealing with existential temporal properties of programs are not on par with that of universal properties. We propose a Horn constraints based method that can not only formalize declaratively but also solve efficiently various problems in formal methods that involve existential (and universal) temporal properties. We apply our metho...     »

Programm Verifikation versucht nachzuweisen, dass ein Programm eine gewünschte Eigenschaft erfüllt. Eine wichtige Klasse von Spezifikationformen in diesem Kontext bilden Temporallogiken. Dennoch sind die Methoden zur Behandlung von existentiellen temporal Eigenschaften nicht so ausgereift wie die zur Behandlung von universellen Eigenschaften. Wir präsentieren eine neuartige Methode basierend auf Horn Klauseln, die nicht nur die Eigenschaften formalisiert sondern auch einen effektiven Ansatz zum Lösen solcher Probleme bereitstellt. Wir wenden unsere Methode an um branching-time temporal Eigenschaften zu überprüfen und Gewinnstrategien für Graph-Spielen auf infinite-state Programmen zu berechnen.     «

Programm Verifikation versucht nachzuweisen, dass ein Programm eine gewünschte Eigenschaft erfüllt. Eine wichtige Klasse von Spezifikationformen in diesem Kontext bilden Temporallogiken. Dennoch sind die Methoden zur Behandlung von existentiellen temporal Eigenschaften nicht so ausgereift wie die zur Behandlung von universellen Eigenschaften. Wir präsentieren eine neuartige Methode basierend auf Horn Klauseln, die nicht nur die Eigenschaften formalisiert sondern auch einen effektiven Ansatz zum...     »