Publications

(2023). Decentralized Stream Runtime Verification for Timed Asynchronous Networks. IEEE Access, pp 84091-84112. IEEE, 2023.

PDF Cite DOI URL

(2023). Runtime verification of real-time event streams using the tool HStriver. Formal Methods in Systems Desing. Springer, 2023.

PDF Cite DOI URL

(2023). Tableaux for Realizability of Safety Specifications. Proc. of the 25th International Symposium on Formal Methods (FM'23), vol 14000 of LNCS, pp. 495–513. Springer, 2023.

PDF Cite DOI URL

(2023). General Anticipatory Monitoring for Temporal Logics on Finite Traces. Proc. of the 23nd Int’l Conference on Runtime Verification (RV'23), vol 14245 of LNCS, pp. 106-125. Springer, Cham, 2023.

PDF Cite DOI URL

(2023). Efficient Reactive Synthesis Using Mode Decomposition. Proc. of the 20th Int’l Colloquium on Theoretical Aspects of Computing (ICTAC'23), vol 14446 of LNCS, pp. 256-275. Springer, Cham, 2023.

PDF Cite DOI URL

(2023). Efficient Loop Conditions for Bounded Model Checking Hyperproperties. Proc. of the 29th Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'23), vol 13993 of LNCS, pp. 66-84. Springer, Cham, 2023.

PDF Cite DOI URL

(2023). Bounded Model Checking for Asynchronous Hyperproperties. Proc. of the 29th Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'23), vol 13993 of LNCS, pp. 29-46. Springer, Cham, 2023.

PDF Cite DOI URL

(2023). Boolean Abstractions for Realizabilty Modulo Theories. Proc. of the 35th International Conference on Computer Aided Verification (CAV'23), vol 13966 of LNCS, pp. 1-24. Springer, Cham, 2023.

PDF Cite DOI URL

(2023). A Stream Runtime Verification Tool with Nested and Retroactive Parametrization. Proc. of the 23nd Int’l Conference on Runtime Verification (RV'23), vol 14245 of LNCS, pp. 351-362. Springer, Cham, 2023.

PDF Cite DOI URL

(2022). Transaction Monitoring of Smart Contracts. Proc. of the 22nd Int’l Conference on Runtime Verification (RV'22), vol 13498 of LNCS, pp. 162-180. Springer, 2022.

PDF Cite DOI URL

(2022). Symbolic Runtime Verification for Monitoring Under Uncertainties and Assumptions. Proc. of 20th Int’l Symp. on Automated Technology for Verification and Analysis (ATVA'22), vol 13505 of LNCS, pp. 117-134. Springer, 2022.

PDF Cite DOI URL

(2022). Setchain: Improving Blockchain Scalability with Byzantine Distributed Sets and Barriers. Proc. of the 2022 IEEE Int’l Conf. on Blockchain (Blockchain'22), pp-87-96, IEEE, 2022.

PDF Cite DOI URL

(2022). Multi: A Formal Playground for Multi-Smart Contract Interaction. Proc. of the 4th Int’l Workshop on Formal Methods for Blockchains (FMBC'2022), vol. 105 of Open Access Series in Informatics (OASIcs), pp 5:1–5:16. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2022.

PDF Cite DOI URL

(2022). Monitorability of Expressive Verdicts. Proc. of the 14th Int’l Symp. on NASA Formal Methods (NFM'22), vol 13260 of LNCS, pp 693-712. Springer, 2022.

PDF Cite DOI URL

(2022). Expressiveness and Decidability of Temporal Logics for Asynchronous Hyperproperties. Proc. of the 33rd International Conference on Concurrency Theory (CONCUR'22), vol. 243 of Leibniz International Proceedings in Informatics (LIPIcs), pp 27:1–27:16, Schloss Dagstuhl Leibniz-Zentrum für Informatik 2022.

PDF Cite DOI URL

(2022). Assumption Monitoring of Temporal Task Planning Using Stream Runtime Verification. Proc. of the 11th Int’l Symp. on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'2022). Verification Principles. Part I, vol. 13701 of LNCS, pp 397-414. Springer, 2022.

PDF Cite DOI URL

(2022). Anticipatory Recurrent Monitoring with Uncertainty and Assumptions. Proc. of the 22nd Int’l Conference on Runtime Verification (RV'22), vol 13498 of LNCS, pp. 181-199. Springer, 2022.

PDF Cite DOI URL

(2021). Synchronous and asynchronous stream runtime verification. Proc. of the 5th ACM Int’l Workshop on Verification and mOnitoring at Runtime EXecution (VORTEX'21), ACM, pp 5-7, 2021.

PDF Cite DOI URL

(2021). Stream runtime verification of real-time event streams with the Striver language. International Journal on Software Tools for Technology Transfer, 23, pp 157-183. Springer.

PDF Cite DOI URL

(2021). Nested Monitors: Monitors as Expressions to Build Monitors. Proc. of the 21st Int’l Conference on Runtime Verification (RV'21), vol 12974 of LNCS, pp 164-183. Springer, 2021.

PDF Cite DOI URL

(2021). HStriver: A Very Functional Extensible Tool for the Runtime Verification of Real-Time Event Streams. Proc. of the 24th Int’l Symp. on Formal Methods (FM'21), vol 13047 of LNCS, pp 563-580.

PDF Cite DOI URL

(2021). HLola: a Very Functional Tool for Extensible Stream Runtime Verification. Proc. of the 27th Int’l Conf on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'21). Part II, vol 12652 of LNCS, pp 349-356. Springer, 2021.

PDF Cite DOI URL

(2021). Bounded Model Checking for Hyperproperties. Proc. of the 27th Int’l Conf on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'21). Part I, vol 12651 of LNCS, pp 94-112. Springer, 2021.

PDF Cite DOI URL

(2021). Asynchronous Extensions of HyperLTL. Proc. of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'21), pp1-13, IEEE.

PDF Cite DOI URL

(2021). Assumption Monitoring Using Runtime Verification for UAV Temporal Task Plan Executions. Proc. of the IEEE Int’l Conf. on Robotics and Automation, (ICRA'21), pp6824-6830, IEEE, 2021.

PDF Cite DOI URL

(2021). A Temporal Logic for Asynchronous Hyperproperties. Proc. of the 33rd Int’l Conf. on Computer Aided Verification (CAV'21), Part I, vol. 12759 of LNCS, pp 694-717. Springer, 2021..

PDF Cite DOI URL

(2020). Unifying the Time-Event Spectrum for Stream Runtime Verification. Proc. of the 20th Int’l Conference on Runtime Verification (RV'20), vol 12399 of LNCS, pp. 462-481. Springer, 2020.

PDF Cite DOI URL

(2020). Runtime verification of real-time event streams under non-synchronized arrival. Software Quality Journal, 28(2):745-787.

PDF Cite DOI URL

(2020). Reliable Smart Contracts. Proc. of the 9th Int’l Symp. on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'2020). Verification. Part III, vol 12478 of LNCS, pp3-8. Springer, 2020.

PDF Cite DOI URL

(2020). Model Checking Timed Hyperproperties in Discrete-Time Systems. Proc. of the 12th NASA Formal Methods Symposium (NFM'2020), vol 12229 of LNCS, pp 311-328, Springer, 2020.

PDF Cite DOI URL

(2020). Gray-Box Monitoring of Hyperproperties with an Application to Privacy. Formal Methods in Systems Desing, p1-34. Springer, 2021.

PDF Cite DOI URL

(2020). Declarative Stream Runtime Verification (hLola). Proc. of the 18th Asian Symposium on Programming Languages and Systems (APLAS'20), vol 12470 of LNCS, pp 25-43. Springer, 2020.

PDF Cite DOI URL

(2019). A survey of challenges for runtime verification from advanced application domains (beyond software). Formal Methods in System Design, Formal Methods in Systems Design 54(3):279-335 (2019).

PDF Cite DOI URL

(2019). Runtime Verification for Timed Event Streams with Partial Information. Proc. of the 19th Int’l Conf. on Runtime Verification (RV'19), vol 11757 of LNCS, pp 273-291, Springer, 2019.

PDF Cite DOI URL

(2019). Decentralized Stream Runtime Verification. Proc. of the 19th Int’l Conf. on Runtime Verification (RV'19), vol 11757 of LNCS, pp 185-201, Springer, 2019.

PDF Cite DOI URL

(2019). Verifying Hyperliveness. Proc. of the 31st Int’l Conf. on Computer Aided Verification (CAV'19), vol 11561 of LNCS, pp 121-139, Springer 2019.

PDF Cite DOI URL

(2019). Gray-Box Monitoring of Hyperproperties. Formal Methods - The Next 30 Years - Third World Congress, FM 2019, , vol 11800 of LNCS, pp 496-424, Springer, 2019.

PDF Cite DOI URL

(2018). Visibly Linear Temporal Logic. Journal of Automated Reasoning, (62)2:177-220, 2018.

PDF Cite DOI URL

(2018). Timed Epistemic Knowledge Bases for Social Networks. Proc. of 22nd Int’l Symposium on Formal Methods (FM'18), vol 10951 of LNCS, pp 185-202, Springer, 2018.

PDF Cite DOI URL

(2018). TeSSLa: Runtime Verification of Non-synchronized Real-Time Streams. Proc. of the 33rd ACM/SIGAPP Symposium on Applied Computing (SAC'18), pp 1925-1933, ACM 2018.

PDF Cite DOI URL

(2018). Striver: Stream Runtime Verification for Real-Time Event-Streams. Proc. of the 18th Int’l Conf. on Runtime Verification (RV'18), vol 11237 of LNCS, pp 282-298, Springer, 2018.

PDF Cite DOI URL

(2018). Runtime Verification for Decentralized and Distributed Systems. Lectures on Runtime Verification – Introductory and Advanced Topics, 2018:176-210.

PDF Cite DOI URL

(2018). Reliable Smart Contracts: State-of-the-Art, Applications, Challenges and Future Directions. Proc. of the 8th Int’l Symp. on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'2018). Verification. Part IV, vol 11247 of LNCS, pp 275-279, Springer, 2018.

PDF Cite DOI URL

(2018). Pipekit: A Deployment Tool with Advanced Scheduling and Inter-Service Communication for Multi-Tier Applications. Proc. of the IEEE Int’l Conf. on Web Services (ICWS'18), pp 379-382, IEEE CS Press, 2018.

PDF Cite DOI URL

(2018). Online and Offline Stream Runtime Verification of Synchronous Systems. Proc. of the 18th Int’l Conf. on Runtime Verification (RV'18), vol 11237 of LNCS, pp 138-163, Springer, 2018.

PDF Cite DOI URL

(2018). Monitoring Hyperproperties by Combining Static Analysis and Runtime Verification. Proc. of the 8th Int’l Symp. on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'2018). Verification. Part II, vol 11245 of LNCS, pp 8-27, Springer, 2018.

PDF Cite DOI URL

(2018). Introduction to the special issue on runtime verification. Formal Methods in Systems Design, 53(1):1-5 (2018).

PDF Cite DOI URL

(2018). i2kit: A Deployment Tool with the Simplicity of Containers and the Security of Virtual Machines. Proc. of the 19th Int’l Conf. on Web Information Systems Engineering (WISE 2018), Part I, Part I, vol 11233 of LNCS, pp 81-95, Springer, 2018.

PDF Cite DOI URL

(2018). COST Action IC1402 Runtime Verification Beyond Monitoring. Proc. of the 18th Int’l Conf. on Runtime Verification (RV'18), vol 11237 of LNCS, pp 18-26, Springer, 2018.

PDF Cite DOI URL

(2017). Parametrized Verification Diagrams: Temporal Verification of Symmetric Parametrized Concurrent Systems. Annals of Mathematics and Artificial Intelligence, 80(3-4): 249-282, 2017.

PDF Cite DOI URL

(2016). Specification of Evolving Privacy Policies for Online Social Networks. Proc. of the 23rd Int’l Symp. on Temporal Representation and Reasoning (TIME'16), pp 77-79, IEEE Computer Society, 2014.

PDF Cite DOI URL

(2016). Special issue on temporal representation and reasoning (TIME'13). Acta Informatica, 53(2): 87-88, 2016.

PDF Cite DOI URL

(2016). Special issue on Rich Models, EU-COST Action IC0901 Rich-Model Toolkit. Acta Informatica, 53(4): 325-326, 2016.

PDF Cite DOI URL

(2016). Foundations of Boolean Stream Runtime Verification. Theoretical Computer Science, 631:118-138.

PDF Cite DOI URL

(2015). Parametrized Invariance for Infinite State Processes. Acta Informatica, 52(6), pp 525–557, 2015.

PDF Cite DOI URL

(2015). Algorithms for Model Checking HyperLTL and HyperCTL*. Proc. of the 27th Int’l Conf. on Computer Aided Verification (CAV'15), vol 9206 of LNCS, pp 30-48, Springer, 2015.

PDF Cite DOI URL

(2014). Visibly Rational Expressions. Acta Informatica, 51(1): 25-49, 2014.

PDF Cite DOI URL

(2014). Visibly Linear Temporal Logic. Proc. of the 7th Int’l Joint Conf. on Automated Reasoning (IJCAR'14), vol 8562 of LNCS, pp 418-433, Springer, 2014.

PDF Cite DOI URL

(2014). Temporal Logics for Hyperproperties. Proc. of the 3rd Conference on Principles of Security and Trust (POST'14), vol 8414 of LNCS, pp 265-284, Springer, 2014.

PDF Cite DOI URL

(2014). Parametrized Verification Diagrams. Proc. of the 21st Int’l Symp. on Temporal Representation and Reasoning (TIME'14), pp132-141, IEEE Computer Society, 2014.

PDF Cite DOI URL

(2014). LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes. Proc. of the 26th Int’l Conf. on Computer Aided Verification (CAV'14), vol 8559 of LNCS, pp 620-627, Springer, 2014.

PDF Cite DOI URL

(2014). Foundations of Boolean Stream Runtime Verification. Proc. of the 14th Int’l Conf. on Runtime Verification (RV'14), vol 8734 of LNCS, pp 64-79, Springer, 2014.

PDF Cite DOI URL

(2014). Formal Verification of Skiplists with Arbitrarily Many Levels. Proc. of the 12th Int’l Symp. on Automated Technology for Verification and Analysis (ATVA), vol 8837 of LNCS, pp 314-329, Springer, 2014.

PDF Cite DOI URL

(2013). Fusing Statecharts and Java. ACM Transactions on Embedded Computing Systems, vol 12, number 1s, pages 45:1-45:21, ACM, 2013.

PDF Cite DOI URL

(2013). Abstracting Runtime Heaps for Program Understanding. IEEE Transactions on Software Engineering, 39(6): 774-786 (2013).

PDF Cite DOI URL

(2012). Ubiquitous Green Computing Techniques for High Demand Applications in Smart Environments. Sensors, vol. 12, issue 8, pp. 10659–10677, ISSN 1424-8220, 2012.

PDF Cite DOI URL

(2012). Visibly Rational Expressions. Proc. of the 32nd Int’l Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'12), vol 18 of Leibniz International Proceedings in Informatics (LIPIcs), pp 211-223, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik 2012.

PDF Cite DOI URL

(2012). Invariant Generation for Parametrized Systems Using Self-reflection. Proc. of the 19th International Symposium on Static Analysis (SAS'12), vol 7460 of Lecture Notes in Computer Science pp146-163, Springer 2012.

PDF Cite DOI URL

(2012). How to Translate Efficiently Extensions of Temporal Logics into Alternating Automata. Proceedings of The 9th International Colloquium on Theoretical Aspects of Computing (ICTAC'12), vol 7521 of LNCS, pp30-45, Springer, 2012.

PDF Cite DOI URL

(2012). Efficient Regular Linear Temporal Logic Using Dualization and Stratification. Proceedings of the 19th International Symposium on Temporal Representation and Reasoning (TIME'12), IEEE Computer Society, 2012.

PDF Cite DOI URL

(2011). A Theory of Skiplists with Applications to the Verification of Concurrent Datatypes. Proc. of the 3rd NASA Formal Methods Symposium (NFM'11), vol 6617 of Lecture Notes in Computer Science, pp343–358, Springer 2011.

PDF Cite DOI URL

(2010). Regular Linear-Time Temporal Logic. Proceedings of the 17th International Symposium on Temporal Representation and Reasoning (TIME'10), pp 3-5, IEEE Computer Society, 2010.

PDF Cite DOI URL

(2010). Regular Linear Temporal Logic with Past. Proc. of the 11th Int’l Conf. on Verification, Model Checking, and Abstract Interpretation, (VMCAI'10), vol. 5944 of LNCS, pp 295-311. Springer, 2010.

PDF Cite DOI URL

(2010). Decision Procedures for the Temporal Verification of Concurrent Lists. Proc. of the 12th Int’l Conf. on Formal Engineering Methods (ICFEM'10), vol. 6447 of LNCS, pp 74-89, Springer, 2010.

PDF Cite DOI URL

(2010). Analyzing the Impact of Change in Multi-threaded Programs. Proc. of the 13th Int’l Conf. on Fundamental Approaches to Software Engineering (FASE'10), vol. 6013 of LNCS, pp 293-307. Springer, 2010.

PDF Cite DOI URL

(2008). The Reaction Algebra: A Formal Language for Event Correlation. Pillars of Computer Science: Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, vol. 4800 of LNCS, pp 586-609, Springer 2008.

PDF Cite DOI URL

(2007). Regular Linear Temporal Logic. Proc. of The 4th Int’l Colloquium on Theoretical Aspects of Computing (ICTAC'07), vol. 4711 of LNCS, pp 291-305. Springer, 2007.

PDF Cite DOI URL

(2007). Deadlock Avoidance for Distributed Real-time and Embedded Systems. Ph.D Thesis, Computer Science Department, Stanford University, May, 2007.

PDF Cite URL

(2007). Generating Efficient Distributed Deadlock Avoidance Controllers. Proc. of the 5th Int’l Workshop on Parallel and Distributed Real-Time Systems (WPDRTS 2007), IEEE Computer Society Press, 2007.

PDF Cite DOI URL

(2007). A Family of Distributed Deadlock Avoidance Protocols and their Reachable State Spaces. Fundamental Approaches to Software Engineering (FASE'07), vol. 4422 of LNCS, pp155-169. Springer, 2007.

PDF Cite DOI URL

(2006). Reusable Models for Timing and Liveness Analysis of Middleware for Distributed Real-Time Embedded Systems. Proc. of the 6th ACM & IEEE Conference on Embedded Software (EMSOFT'06), pp252-261. ACM Press, 2006.

PDF Cite DOI URL

(2006). On Efficient Distributed Deadlock Avoidance for Distributed Real-Time and Embedded Systems. Proc. of the 20th IEEE International Parallel and Distributed Processing Symposium (IPDPS'06), IEEE Computer Society Press, 2006.

PDF Cite DOI URL

(2006). Efficient Distributed Deadlock Avoidance with Liveness Guarantees. Proc. of the 6th ACM & IEEE Conference on Embedded Software (EMSOFT'06), pp12-20. ACM Press, 2006.

PDF Cite DOI URL

(2006). Distributed Priority Inheritance for Real-Time and Embedded Systems. Proc. of the 10th Int’l Conf. On Principles Of Distributed Systems (OPODIS'06), vol. 4305 of LNCS, pp110-125. Springer, 2006.

PDF Cite DOI URL

(2005). Final Semantics for Event-Pattern Reactive Programs. Proc. of the First Int’l Conf. in Algebra and Coalgebra in Computer Science (CALCO'05), vol 3629 of LNCS, pp364-378. Springer, 2005.

PDF Cite DOI URL

(2005). Thread Allocation Protocols for Distributed Real-time and Embedded Systems. Proc. of the 25th IFIP WG 2.6 International Conference on Formal for Networked and Distributed Systems (FORTE'05), vol. 3731 of LNCS, pp 159-173. Springer, 2005.

PDF Cite DOI URL

(2005). LOLA: Runtime Monitoring of Synchronous Systems. Proc. of the 12th Int’l Symposium of Temporal Representation and Reasoning (TIME 2005), pp. 166-174. IEEE Computer Society Press, 2005.

PDF Cite DOI URL

(2005). Expressive Completeness of an Event-Pattern Reactive Programming Language. Proc. of the 25th IFIP WG 2.6 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'05), vol. 3731 of LNCS, pp 529-532. Springer, 2005.

PDF Cite DOI URL

(2003). Event Correlation: Language and Semantics. Proc. of the 3rd Int’l Conf. on Embedded Software (EMSOFT'03), vol 2855 of LNCS, pp 323-339. Springer, 2003.

PDF Cite DOI URL