Article

The temporal logic of programs

Author:

Amir PnueliAuthors Info & Claims

SFCS '77: Proceedings of the 18th Annual Symposium on Foundations of Computer Science

Pages 46 - 57

https://doi.org/10.1109/SFCS.1977.32

Published: 30 September 1977 Publication History

Publisher Site

Abstract

A unified approach to program verification is suggested, which applies to both sequential and parallel programs. The main proof method suggested is that of temporal reasoning in which the time dependence of events is the basic concept. Two formal systems are presented for providing a basis for temporal reasoning. One forms a formalization of the method of intermittent assertions, while the other is an adaptation of the tense logic system Kb, and is particularly suitable for reasoning about concurrent programs.

Cited By

View all

Yao YIraci GChuang CBalzer SZiarek L(2025)Semantic Logical Relations for Timed Message-Passing ProtocolsProceedings of the ACM on Programming Languages10.1145/37048959:POPL(1750-1781)Online publication date: 9-Jan-2025
https://doi.org/10.1145/3704895
Heim PDimitrova R(2025)Translation of Temporal Logic for Efficient Infinite-State Reactive SynthesisProceedings of the ACM on Programming Languages10.1145/37048889:POPL(1536-1567)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704888
Veanes MBall TEbner GZhuchko E(2025)Symbolic Automata: Omega-Regularity Modulo TheoriesProceedings of the ACM on Programming Languages10.1145/37048389:POPL(33-66)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704838
Show More Cited By

The temporal logic of programs
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
2. Theory of computation
  1. Semantics and reasoning

Recommendations

Constructive linear-time temporal logic: Proof systems and Kripke semantics

In this paper we study a version of constructive linear-time temporal logic (LTL) with the ''next'' temporal operator. The logic is originally due to Davies, who has shown that the proof system of the logic corresponds to a type system for binding-time ...
A Paraconsistent Linear-time Temporal Logic

Inconsistency-tolerant reasoning and paraconsistent logic are of growing importance not only in Knowledge Representation, AI and other areas of Computer Science, but also in Philosophical Logic. In this paper, a new logic, paraconsistent linear-time ...
Querying datalog programs with temporal logic

Temporal logic queries on Datalog and negated Datalog programs are studied, and their relationship to Datalog queries on these programs is explored. It is shown that, in general, temporal logic queries have more expressive power than Datalog queries on ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

SFCS '77: Proceedings of the 18th Annual Symposium on Foundations of Computer Science

September 1977

269 pages

Publisher

IEEE Computer Society

United States

Publication History

Published: 30 September 1977

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1,187
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Yao YIraci GChuang CBalzer SZiarek L(2025)Semantic Logical Relations for Timed Message-Passing ProtocolsProceedings of the ACM on Programming Languages10.1145/37048959:POPL(1750-1781)Online publication date: 9-Jan-2025
https://doi.org/10.1145/3704895
Heim PDimitrova R(2025)Translation of Temporal Logic for Efficient Infinite-State Reactive SynthesisProceedings of the ACM on Programming Languages10.1145/37048889:POPL(1536-1567)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704888
Veanes MBall TEbner GZhuchko E(2025)Symbolic Automata: Omega-Regularity Modulo TheoriesProceedings of the ACM on Programming Languages10.1145/37048389:POPL(33-66)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704838
Yu YXu YHuang KLiu JBalzarotti DXu W(2024)TAPFixerProceedings of the 33rd USENIX Conference on Security Symposium10.5555/3698900.3699177(4945-4962)Online publication date: 14-Aug-2024
https://dl.acm.org/doi/10.5555/3698900.3699177
Svoboda JBansal SChatterjee KSalakhutdinov RKolter ZHeller KWeller AOliver NScarlett JBerkenkamp F(2024)Reinforcement learning from reachability specificationsProceedings of the 41st International Conference on Machine Learning10.5555/3692070.3693998(47331-47344)Online publication date: 21-Jul-2024
https://dl.acm.org/doi/10.5555/3692070.3693998
Leahy KMann MSerlin ZSalakhutdinov RKolter ZHeller KWeller AOliver NScarlett JBerkenkamp F(2024)Run-time task composition with safety semanticsProceedings of the 41st International Conference on Machine Learning10.5555/3692070.3693119(26241-26258)Online publication date: 21-Jul-2024
https://dl.acm.org/doi/10.5555/3692070.3693119
Jamroga WMittelmann MMurano APerelli GDastani MSichman JAlechina NDignum V(2024)Playing Quantitative Games Against an Authority: On the Module Checking ProblemProceedings of the 23rd International Conference on Autonomous Agents and Multiagent Systems10.5555/3635637.3662947(926-934)Online publication date: 6-May-2024
https://dl.acm.org/doi/10.5555/3635637.3662947
Hyland DGutierrez JShankaranarayanan KWooldridge MDastani MSichman JAlechina NDignum V(2024)Rational Verification with Quantitative Probabilistic GoalsProceedings of the 23rd International Conference on Autonomous Agents and Multiagent Systems10.5555/3635637.3662941(871-879)Online publication date: 6-May-2024
https://dl.acm.org/doi/10.5555/3635637.3662941
Catta DLeneutre JMalvone VMurano ADastani MSichman JAlechina NDignum V(2024)Obstruction Alternating-time Temporal Logic: A Strategic Logic to Reason about Dynamic ModelsProceedings of the 23rd International Conference on Autonomous Agents and Multiagent Systems10.5555/3635637.3662875(271-280)Online publication date: 6-May-2024
https://dl.acm.org/doi/10.5555/3635637.3662875
Belardinelli FJamroga WMittelmann MMurano ADastani MSichman JAlechina NDignum V(2024)Verification of Stochastic Multi-Agent Systems with Forgetful StrategiesProceedings of the 23rd International Conference on Autonomous Agents and Multiagent Systems10.5555/3635637.3662863(160-169)Online publication date: 6-May-2024
https://dl.acm.org/doi/10.5555/3635637.3662863
Show More Cited By

Abstract

Cited By

Recommendations

Constructive linear-time temporal logic: Proof systems and Kripke semantics

A Paraconsistent Linear-time Temporal Logic

Querying datalog programs with temporal logic

Comments

Information

Published In

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Share

Share this Publication link

Share on social media

Affiliations