More Web Proxy on the site http://driver.im/

research-article

Runtime Verification for LTL and TLTL

Authors:

Martin Leucker,

Christian SchallhartAuthors Info & Claims

ACM Transactions on Software Engineering and Methodology (TOSEM), Volume 20, Issue 4

Article No.: 14, Pages 1 - 64

https://doi.org/10.1145/2000799.2000800

Published: 01 September 2011 Publication History

Abstract

This article studies runtime verification of properties expressed either in lineartime temporal logic (LTL) or timed lineartime temporal logic (TLTL). It classifies runtime verification in identifying its distinguishing features to model checking and testing, respectively. It introduces a three-valued semantics (with truth values true, false, inconclusive) as an adequate interpretation as to whether a partial observation of a running system meets an LTL or TLTL property.

For LTL, a conceptually simple monitor generation procedure is given, which is optimal in two respects: First, the size of the generated deterministic monitor is minimal, and, second, the monitor identifies a continuously monitored trace as either satisfying or falsifying a property as early as possible. The feasibility of the developed methodology is demontrated using a collection of real-world temporal logic specifications. Moreover, the presented approach is related to the properties monitorable in general and is compared to existing concepts in the literature. It is shown that the set of monitorable properties does not only encompass the safety and cosafety properties but is strictly larger.

For TLTL, the same road map is followed by first defining a three-valued semantics. The corresponding construction of a timed monitor is more involved, yet, as shown, possible.

References

[1]

Aho, A., Sethi, R., and Ullman, J. 1986. Compilers: Principles and Techniques and Tools. Addison-Wesley.

Digital Library

[2]

Allan, C., Avgustinov, P., Christensen, A. S., Hendren, L. J., Kuzins, S., Lhoták, O., de Moor, O., Sereni, D., Sittampalam, G., and Tibble, J. 2005. Adding trace matching with free variables to aspectj. In Proceedings of the Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA). 345--364.

Digital Library

[3]

Alpern, B. and Schneider, F. B. 1987. Recognizing safety and liveness. Distrib. Comput. 2, 3, 117--126.

Digital Library

[4]

Alur, R. and Dill, D. L. 1994. A theory of timed automata. Theor. Comput. Sci. 126, 2, 183--235.

Digital Library

[5]

Alur, R., Courcoubetis, C., and Dill, D. L. 1993. Model-checking in dense real-time. Inform. Computat. 104, 1, 2--34.

Digital Library

[6]

Alur, R., Fix, L., and Henzinger, T. A. 1999. Event-clock automata: a determinizable class of timed automata. Theor. Comput. Sci. 211, 1--2, 253--273.

Digital Library

[7]

Barbon, F., Traverso, P., Pistore, M., and Trainotti, M. 2006. Run-time monitoring of instances and classes of web service compositions. In Proceedings of the International Conference on Web Services (ICWS). IEEE Computer Society, 63--71.

Digital Library

[8]

Baresi, L., Guinea, S., and Pasquale, L. 2008. Towards a unified framework for the monitoring and recovery of bpel processes. In Proceedings of the Workshop on Testing, Analysis, and Verification of Web Services and Applications (TAV-WEB). T. Bultan and T. Xie Eds., ACM, 15--19.

Digital Library

[9]

Barringer, H., Goldberg, A., Havelund, K., and Sen, K. 2004. Program monitoring with ltl in eagle. In Proceedings of the International Parallel and Distributed Processing Symposium (IPDPS).

[10]

Barringer, H., Rydeheard, D. E., and Havelund, K. 2007. Rule systems for run-time monitoring: From eagle to ruler. In International Workshop on Runtime Verification (RV). Lecture Notes in Computer Science, vol. 4839, 111--125.

Digital Library

[11]

Bauer, A., Leucker, M., and Schallhart, C. 2006a. Model-based runtime analysis of reactive distributed systems. In Proceedings of the Australian Software Engineering Conference (ASWEC). IEEE Computer Society, 243--252.

Digital Library

[12]

Bauer, A., Leucker, M., and Schallhart, C. 2006b. Monitoring of real-time properties. In Proceedings of the 26th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). S. Arun-Kumar and N. Garg Eds., Lecture Notes in Computer Science, vol. 4337, Springer-Verlag, 260--272.

Digital Library

[13]

Bauer, A., Leucker, M., and Schallhart, C. 2007. The good, the bad, and the ugly---but how ugly is ugly? In Proceedings of the International Workshop on Runtime Verification (RV). Lecture Notes in Computer Science, vol. 4839, Springer-Verlag, 126--138.

Digital Library

[14]

Bauer, A., Leucker, M., and Schallhart, C. 2010. Comparing LTL semantics for runtime verification. J. Logic Comput. 20, 3, 651--674.

Digital Library

[15]

Behrmann, G., David, A., Larsen, K. G., Håkansson, J., Pettersson, P., Yi, W., and Hendriks, M. 2006. Uppaal 4.0. In Proceedings of the International Conference on the Quantitative Evaluaiton of Systems (QEST). IEEE Computer Society, 125--126.

Digital Library

[16]

Bengtsson, J., Larsen, K. G., Larsson, F., Pettersson, P., and Yi, W. 1996. UPPAAL: a tool suite for the automatic verification of real-time systems. In Hybrid Systems III. R. Alur, T. A. Henzinger, and E. D. Sontag Eds., Lecture Notes in Computer Science, vol. 1066., Springer-Verlag, 232--243.

Digital Library

[17]

Berg, T., Jonsson, B., Leucker, M., and Saksena, M. 2003. Insights to Angluin’s learning. In Proceedings of the International Workshop on Software Verification and Validation (SVV). Electronic Notes in Theoretical Computer Science, vol. 118, 3--18.

[18]

Biere, A., Cimatti, A., Clarke, E. M., and Zhu, Y. 1999. Symbolic model checking without BDDs. In Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS). R. Cleaveland Ed., Lecture Notes in Computer Science, vol. 1579, Springer, 193--207.

Digital Library

[19]

Biere, A., Cimatti, A., Clarke, E., Strichman, O., and Zhu, Y. 2003. Bounded model checking. In Advances in Computers, vol. 58. Academic Press, 118--149.

[20]

Bodden, E. 2004. A lightweight ltl runtime verification tool for java. In OOPSLA Companion. J. M. Vlissides and D. C. Schmidt Eds., ACM, 306--307.

Digital Library

[21]

Bouyer, P., Chevalier, F., and D’Souza, D. 2005. Fault diagnosis using timed automata. In Proceedings of the 8th International Conference on Foundations of Software Science and Computational Structures (FoSSaCS). V. Sassone Ed., Lecture Notes in Computer Science, vol. 3441, Springer, 219--233.

Digital Library

[22]

Bryant, R. E. 1985. Symbolic manipulation of boolean functions using a graphical representation. In Proceedings of the 22nd ACM/IEEE Design Automation Conference. IEEE Computer Society Press, 688--694.

Digital Library

[23]

Büchi, J. 1962. On a decision method in restricted second order arithmetic. In Proceedings of the International Congress on Logic, Methodology, and Philosophy of Science. 1--11.

[24]

Chaudhuri, S. and Alur, R. 2007. Instrumenting c programs with nested word monitors. In Proceedings of the International SPIN Workshop. D. Bosnacki and S. Edelkamp Eds., Lecture Notes in Computer Science, vol. 4595, Springer, 279--283.

Digital Library

[25]

Chechik, M., Devereux, B., and Gurfinkel, A. 2001. Model-checking infinite state-space systems with fine-grained abstractions using spin. In Proceedings of the International SPIN Workshop. M. B. Dwyer Ed., Lecture Notes in Computer Science, vol. 2057, Springer, 16--36.

Digital Library

[26]

Chen, F. and Rosu, G. 2003. Towards monitoring-oriented programming: A paradigm combining specification and implementation. Electron. Notes Theor. Comput. Sci. 89, 2.

[27]

Chen, F. and Roşu, G. 2007. MOP: An Efficient and Generic Runtime Verification Framework. In Proceedings of the Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA). 569--588.

Digital Library

[28]

Chow, T. S. 1978. Testing software design modeled by finite-state machines. IEEE Trans. Softw. Engin 4, 3, 178--187.

Digital Library

[29]

Clarke, E. M., Grumberg, O., and Peled, D. A. 1999. Model Checking. MIT Press, Cambridge, MA.

Digital Library

[30]

d’Amorim, M. and Rosu, G. 2005. Efficient monitoring of omega-languages. In Proceedings of the International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 3576, 364--378.

Digital Library

[31]

D’Angelo, B., Sankaranarayanan, S., Sánchez, C., Robinson, W., Finkbeiner, B., Sipma, H. B., Mehrotra, S., and Manna, Z. 2005. LOLA: Runtime monitoring of synchronous systems. In Proceedings of the International Symposium on Temporal Representation and Reasoning (TIME). 166--174.

Digital Library

[32]

Delgado, N., Gates, A. Q., and Roach, S. 2004. A taxonomy and catalog of runtime software-fault monitoring tools. IEEE Trans. Softw. Engin. 30, 12, 859--872.

Digital Library

[33]

Dewhurst, S. 2002. C++ Gotchas: Avoiding Common Problems in Coding and Design. Addison-Wesley Longman Publishing Co., Inc., Boston, MA.

Digital Library

[34]

Dill, D. L. 1989. Timing assumptions and verification of finite-state concurrent systems. In Automatic Verification Methods for Finite State Systems. J. Sifakis Ed., Lecture Notes in Computer Science, vol. 407, Springer, 197--212.

Digital Library

[35]

D’Souza, D. 2003. A logical characterisation of event clock automata. Int. J. Found. Comput. Sci. 14, 4, 625--639.

[36]

Dwyer, M. B., Avrunin, G. S., and Corbett, J. C. 1999. Patterns in property specifications for finite-state verification. In Proceedings of the International Conference on Software Engineering (ICSE). IEEE, Computer Society Press, 411--420.

Digital Library

[37]

Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., and Campenhout, D. V. 2003. Reasoning with temporal logic on truncated paths. In Proceedings of the International Conference Computer Aided Verification (CAV). W. A. H. Jr. and F. Somenzi Eds., Lecture Notes in Computer Science, vol. 2725, Springer, 27--39.

[38]

Erlingsson, Ú. and Schneider, F. B. 2000. Sasi enforcement of security policies: A retrospective. Proceedings of the DARPA Information Survivability Conference and Exposition 2, 1287.

[39]

Finkbeiner, B. and Sipma, H. 2004. Checking finite traces using alternating automata. Form. Meth. Syst. Des. 24, 2, 101--127.

Digital Library

[40]

Fritz, C. 2003. Constructing Büchi automata from linear temporal logic using simulation relations for alternating büchi automata. In Proceedings of the International Conference on Implementation and Application of Automata (CIAA). O. H. Ibarra and Z. Dang Eds., Lecture Notes in Computer Science, vol. 2759, Springer, 35--48.

Digital Library

[41]

Gastin, P. and Oddoux, D. 2001. Fast LTL to Büchi automata translation. In Proceedings of the 13th International Conference on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 2102.

Digital Library

[42]

Geilen, M. 2001. On the construction of monitors for temporal logic properties. Electron. Notes Theor. Comput. Sci. 55, 2.

[43]

Giannakopoulou, D. and Havelund, K. 2001a. Automata-based verification of temporal properties on running programs. In Proceedings of the International Conference on Automated Software Engineering (ASE). IEEE Computer Society, 412--416.

Digital Library

[44]

Giannakopoulou, D. and Havelund, K. 2001b. Runtime analysis of linear temporal logic specifications. Tech. rep. 01.21, RIACS/USRA.

Digital Library

[45]

Goldsmith, S., O’Callahan, R., and Aiken, A. 2005. Relational queries over program traces. In Proceedings of the Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA). 385--402.

Digital Library

[46]

Gollu, A., Puri, A., and Varaiya, P. 1994. Discretization of timed automata. In Proceedings of the 33rd IEEE Conference on Decision and Control. 957--958.

[47]

Grinchtein, O. and Leucker, M. 2008. Network invariants for real-time systems. Form. Asp. Comput. 20, 619--635.

[48]

Håkansson, J., Jonsson, B., and Lundqvist, O. 2003. Generating online test oracles from temporal logic specifications. J. Softw. Tools Technol. Transfer 4, 4, 456--471.

Digital Library

[49]

Havelund, K. and Rosu, G. 2001. Monitoring Java Programs with Java PathExplorer. Electron. Notes Theor. Comput. Sci. 55, 2.

[50]

Havelund, K. and Rosu, G. 2002. Synthesizing Monitors for Safety Properties. In Proceedings of the Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 2280, 342--356.

Digital Library

[51]

Havelund, K. and Rosu, G. 2004. Efficient monitoring of safety properties. J. Softw. Tools Technol. Transfer 6, 2, 158--173.

Digital Library

[52]

Hopcroft, J. 1971. An n log n algorithm for minimizing states in a finite automation. In Theory of Machines and Computations. 189--196.

[53]

Kamp, H. W. 1968. Tense logic and the theory of linear order. Ph.D. thesis, University of California, Los Angeles.

[54]

Kim, M., Kannan, S., Lee, I., Sokolsky, O., and Viswanathan, M. 2002. Computational analysis of run-time monitoring/fundamentals of java-mac. Electron. Notes Theor. Comput. Sci. 70, 4.

[55]

Kim, M., Viswanathan, M., Kannan, S., Lee, I., and Sokolsky, O. 2004. Java-mac: A run-time assurance approach for java programs. Form. Meth. Syst. Des. 24, 2, 129--155.

Digital Library

[56]

Kopetz, H. 1991. Event-triggered versus time-triggered real-time systems. In Operating Systems of the 90s and Beyond. A. I. Karshmer and J. Nehmer Eds., Lecture Notes in Computer Science, vol. 563, Springer, 87--101.

Digital Library

[57]

Kupferman, O. and Vardi, M. Y. 2001. Model checking of safety properties. Form. Meth. Syst. Des. 19, 3, 291--314.

Digital Library

[58]

Lamport, L. 1977. Proving the correctness of multiprocess programs. IEEE Trans. Softw. Engin. 3, 2, 125--143.

Digital Library

[59]

Lichtenstein, O. and Pnueli, A. 1985. Checking that finite state concurrent programs satisfy their linear specification. In Proceedings of the Conference on Principles of Programming Languages (POPL). ACM, New York, 97--107.

Digital Library

[60]

Maler, O. and Nickovic, D. 2004. Monitoring temporal properties of continuous signals. In Proceedings of the Joint International Conferences on Formal Modelling and Analysis of Timed Systems/Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems (FORMATS/FTRTFT). Y. Lakhnech and S. Yovine Eds., Lecture Notes in Computer Science, vol. 3253, Springer, 152--166.

[61]

Manna, Z. and Pnueli, A. 1995. Temporal Verification of Reactive Systems: Safety. Springer, New York.

Digital Library

[62]

Markey, N. and Schnoebelen, P. 2003. Model checking a path. In Proceedings of the Conference on Concurrency Theory (CONCUR). Lecture Notes in Computer Science, vol. 2761, 248--262.

[63]

Martin, M. C., Livshits, V. B., and Lam, M. S. 2005. Finding application errors and security flaws using pql: a program query language. In Proceedings of the Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA). 365--383.

Digital Library

[64]

Peled, D., Vardi, M., and Yannakakis, M. 1999. Black box checking. In Proceedings of the Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols and Protocol Specification, Testing and Verification (FORTE/PSTV). Kluwer, 225--240.

Digital Library

[65]

Pnueli, A. 1977. The temporal logic of programs. In Proceedings of the Symposium on the Foundations of Computer Science (FOCS). IEEE Computer Society Press, 46--57.

Digital Library

[66]

Pnueli, A. and Zaks, A. 2006. PSL model checking and run-time verification via testers. In Proceedings of the International Symposium on Formal Methods (FM). J. Misra, T. Nipkow, and E. Sekerinski Eds., Lecture Notes in Computer Science, vol. 4085, Springer, 573--586.

Digital Library

[67]

Raskin, J.-F. 1999. Logics, automata and classical theories for deciding real-time. Ph.D. thesis, Namur, Belgium.

[68]

Raskin, J.-F. and Schobbens, P.-Y. 1999. The logic of event clocks---decidability, complexity and expressiveness. J. Autom. Lang. Combina. 4, 3, 247--286.

Digital Library

[69]

Robinson, W. 2006. A requirements monitoring framework for enterprise systems. Require. Engin. 11, 1, 17--41.

Digital Library

[70]

Rosu, G. and Bensalem, S. 2006. Allen linear (interval) temporal logic - translation to LTL and monitor synthesis. In Proceedings of the International Conference on Computer Aided Verification (CAV). T. Ball and R. B. Jones Eds., Lecture Notes in Computer Science, vol. 4144, Springer, 263--277.

Digital Library

[71]

Schwoon, S. and Esparza, J. 2005. A note on on-the-fly verification algorithms. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 3440, 174--190.

Digital Library

[72]

Sen, K. and Rosu, G. 2003. Generating optimal monitors for extended regular expressions. Electron. Notes Theor. Comput. Sci. 89, 2.

[73]

Sistla, A. P. and Clarke, E. M. 1985. Complexity of propositional temporal logics. J. ACM 32, 733--749.

Digital Library

[74]

Stolz, V. and Bodden, E. 2006. Temporal assertions using AspectJ. Electron. Notes Theor. Comput. Sci. 144, 4, 109--124.

Digital Library

[75]

Stroustrup, B. 2000. The C++ Programming Language Special Ed. Addison-Wesley, Boston, MA.

Digital Library

[76]

Tarjan, R. 1972. Depth-first search and linear graph algorithms. SIAM J. Comput. 1, 2, 146--160.

Digital Library

[77]

Thati, P. and Rosu, G. 2005. Monitoring algorithms for metric temporal logic specifications. Electron. Notes Theor. Comput. Sci. 113, 145--162.

Digital Library

[78]

Tripakis, S. 2002. Fault diagnosis for timed automata. In Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT). W. Damm and E.-R. Olderog Eds., Lecture Notes in Computer Science, vol. 2469, Springer, 205--224.

Digital Library

[79]

Tripakis, S. and Yovine, S. 2001. Analysis of timed systems using time-abstracting bisimulations. Form. Meth. Syst. Des. 18, 1, 25--68.

Digital Library

[80]

Vardi, M. Y. 1996. An automata-theoretic approach to linear temporal logic. In Logics for Concurrency: Structure Versus Automata. Lecture Notes in Computer Science, vol. 1043, 238--266.

Digital Library

[81]

Vardi, M. Y. and Wolper, P. 1986. An automata-theoretic approach to automatic program verification. In Proceedings of the Symposium on Logic in Computer Science (LICS). IEEE Computer Society Press, 332--345.

[82]

Vasilevski, M. 1973. Failure diagnosis of automata. Cybernetic 9, 4, 653--665.

Cited By

Ferrando ACardoso R(2025)Towards partial monitoring: Never too early to give inScience of Computer Programming10.1016/j.scico.2024.103220240(103220)Online publication date: Mar-2025
https://doi.org/10.1016/j.scico.2024.103220
Beutner RFinkbeiner BFrenkel HMetzger NDastani MSichman JAlechina NDignum V(2024)Monitoring Second-Order HyperpropertiesProceedings of the 23rd International Conference on Autonomous Agents and Multiagent Systems10.5555/3635637.3662865(180-188)Online publication date: 6-May-2024
https://dl.acm.org/doi/10.5555/3635637.3662865
Amjad Rvan Glabbeek RO'Connor L(2024)Semantics for Linear-time Temporal Logic with Finite ObservationsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.412.4412(35-50)Online publication date: 22-Nov-2024
https://doi.org/10.4204/EPTCS.412.4
Show More Cited By

Recommendations

Optimized temporal monitors for SystemC

SystemC is a modeling language built as an extension of C++ . Its growing popularity and the increasing complexity of designs have motivated research efforts aimed at the verification of SystemC models using assertion-based verification (ABV), where ...
A lightweight LTL runtime verification tool for java
OOPSLA '04: Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications

Runtime verification is a special form of runtime testing, employing formal methods and languages. In this work, we utilize next-time free linear-time temporal logic (LTL\textbackslash X) as formal framework. The discipline serves the purpose of ...
Verifying data- and control-oriented properties combining static and runtime verification: theory and tools

Static verification techniques are used to analyse and prove properties about programs before they are executed. Many of these techniques work directly on the source code and are used to verify data-oriented properties over all possible executions. The ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Software Engineering and Methodology

ACM Transactions on Software Engineering and Methodology Volume 20, Issue 4

September 2011

242 pages

ISSN:1049-331X

EISSN:1557-7392

DOI:10.1145/2000799

Issue’s Table of Contents

Copyright © 2011 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 September 2011

Accepted: 01 August 2009

Revised: 01 July 2009

Received: 01 September 2008

Published in TOSEM Volume 20, Issue 4

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

398
Total Citations
View Citations
2,385
Total Downloads

Downloads (Last 12 months)203
Downloads (Last 6 weeks)14

Reflects downloads up to 26 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ferrando ACardoso R(2025)Towards partial monitoring: Never too early to give inScience of Computer Programming10.1016/j.scico.2024.103220240(103220)Online publication date: Mar-2025
https://doi.org/10.1016/j.scico.2024.103220
Beutner RFinkbeiner BFrenkel HMetzger NDastani MSichman JAlechina NDignum V(2024)Monitoring Second-Order HyperpropertiesProceedings of the 23rd International Conference on Autonomous Agents and Multiagent Systems10.5555/3635637.3662865(180-188)Online publication date: 6-May-2024
https://dl.acm.org/doi/10.5555/3635637.3662865
Amjad Rvan Glabbeek RO'Connor L(2024)Semantics for Linear-time Temporal Logic with Finite ObservationsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.412.4412(35-50)Online publication date: 22-Nov-2024
https://doi.org/10.4204/EPTCS.412.4
Serbinowska SPotteiger NTumlin AJohnson T(2024)Verification of Behavior Trees with Contingency MonitorsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.411.4411(56-72)Online publication date: 21-Nov-2024
https://doi.org/10.4204/EPTCS.411.4
Tripuramallu DAnand APinisetty SPearce HRoop PAncona DAudrito G(2024)Runtime Verified Neural Networks for Cyber-Physical SystemsProceedings of the 7th ACM International Workshop on Verification and Monitoring at Runtime Execution10.1145/3679008.3685547(44-51)Online publication date: 13-Sep-2024
https://dl.acm.org/doi/10.1145/3679008.3685547
Dawes JBianculli Dd'Amorim M(2024)Checking Complex Source Code-Level Constraints using Runtime VerificationCompanion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering10.1145/3663529.3663845(255-265)Online publication date: 10-Jul-2024
https://dl.acm.org/doi/10.1145/3663529.3663845
Hallé S(2024)Column: Is Theory (Still) Welcome in Software Engineering Research?ACM SIGSOFT Software Engineering Notes10.1145/3650142.365014849:2(19-21)Online publication date: 3-Apr-2024
https://dl.acm.org/doi/10.1145/3650142.3650148
Schöpp UFaghih FBandopadhyay SJoumaa HIbrahim AXu CYe XDimitrakos TNiu JVaidya J(2024)Static and Dynamic Analysis of a Usage Control SystemProceedings of the 29th ACM Symposium on Access Control Models and Technologies10.1145/3649158.3657038(59-70)Online publication date: 24-Jun-2024
https://dl.acm.org/doi/10.1145/3649158.3657038
Stratan CDawes JBianculli DFuria CLopes APlat NGnesi S(2024)Diagnosing Violations of Time-based Properties Captured in iCFTLProceedings of the 2024 IEEE/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE)10.1145/3644033.3644375(33-43)Online publication date: 14-Apr-2024
https://dl.acm.org/doi/10.1145/3644033.3644375
Schirmer SSingh JJensen EDauer JFinkbeiner BSankaranarayanan S(2024)Temporal Behavior Trees: Robustness and SegmentationProceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control10.1145/3641513.3650180(1-14)Online publication date: 14-May-2024
https://dl.acm.org/doi/10.1145/3641513.3650180
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents