4 Search Results for "Kamburjan, Eduard"

Document
DOI: 10.4230/LIPIcs.CONCUR.2023.9
Compositional Correctness and Completeness for Symbolic Partial Order Reduction

Authors: Åsmund Aqissiaq Arild Kløvstad, Eduard Kamburjan, and Einar Broch Johnsen

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
Partial Order Reduction (POR) and Symbolic Execution (SE) are two fundamental abstraction techniques in program analysis. SE is particularly useful as a state abstraction technique for sequential programs, while POR addresses equivalent interleavings in the execution of concurrent programs. Recently, several promising connections between these two approaches have been investigated, which result in symbolic partial order reduction: partial order reduction of symbolically executed programs. In this work, we provide compositional notions of completeness and correctness for symbolic partial order reduction. We formalize completeness and correctness for (1) abstraction over program states and (2) trace equivalence, such that the abstraction gives rise to a complete and correct SE, the trace equivalence gives rise to a complete and correct POR, and their combination results in complete and correct symbolic partial order reduction. We develop our results for a core parallel imperative programming language and mechanize the proofs in Coq.
Cite as

Åsmund Aqissiaq Arild Kløvstad, Eduard Kamburjan, and Einar Broch Johnsen. Compositional Correctness and Completeness for Symbolic Partial Order Reduction. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{klvstad_et_al:LIPIcs.CONCUR.2023.9,
  author =	{Kl{\o}vstad, \r{A}smund Aqissiaq Arild and Kamburjan, Eduard and Johnsen, Einar Broch},
  title =	{{Compositional Correctness and Completeness for Symbolic Partial Order Reduction}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{9:1--9:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.9},
  URN =		{urn:nbn:de:0030-drops-190035},
  doi =		{10.4230/LIPIcs.CONCUR.2023.9},
  annote =	{Keywords: Symbolic Execution, Coq, Trace Semantics, Partial Order Reduction}
}
Document
Experience Paper
DOI: 10.4230/LIPIcs.ECOOP.2023.40
On Using VeriFast, VerCors, Plural, and KeY to Check Object Usage (Experience Paper)

Authors: João Mota, Marco Giunti, and António Ravara

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
Typestates are a notion of behavioral types that describe protocols for stateful objects, specifying the available methods for each state. Ensuring methods are called in the correct order (protocol compliance), and that, if and when the program terminates, all objects are in the final state (protocol completion) is crucial to write better and safer programs. Objects of this kind are commonly shared among different clients or stored in collections, which may also be shared. However, statically checking protocol compliance and completion when objects are shared is challenging. To evaluate the support given by state of the art verification tools in checking the correct use of shared objects with protocol, we present a survey on four tools for Java: VeriFast, VerCors, Plural, and KeY. We describe the implementation of a file reader, linked-list, and iterator, check for each tool its ability to statically guarantee protocol compliance and completion, even when objects are shared in collections, and evaluate the programmer’s effort in making the code acceptable to these tools. With this study, we motivate the need for lightweight methods to verify the presented kinds of programs.
Cite as

João Mota, Marco Giunti, and António Ravara. On Using VeriFast, VerCors, Plural, and KeY to Check Object Usage (Experience Paper). In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 40:1-40:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{mota_et_al:LIPIcs.ECOOP.2023.40,
  author =	{Mota, Jo\~{a}o and Giunti, Marco and Ravara, Ant\'{o}nio},
  title =	{{On Using VeriFast, VerCors, Plural, and KeY to Check Object Usage}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{40:1--40:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.40},
  URN =		{urn:nbn:de:0030-drops-182330},
  doi =		{10.4230/LIPIcs.ECOOP.2023.40},
  annote =	{Keywords: Java, Typestates, VeriFast, VerCors, Plural, KeY}
}
Document
DOI: 10.4230/LITES.8.2.4
A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems

Authors: Eduard Kamburjan, Stefan Mitsch, and Reiner Hähnle

Published in: LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2

Abstract
Designing and modeling complex cyber-physical systems (CPS) faces the double challenge of combined discrete-continuous dynamics and concurrent behavior. Existing formal modeling and verification languages for CPS expose the underlying proof search technology. They lack high-level structuring elements and are not efficiently executable. The ensuing modeling gap renders formal CPS models hard to understand and to validate. We propose a high-level programming-based approach to formal modeling and verification of hybrid systems as a hybrid extension of an Active Objects language. Well-structured hybrid active programs and requirements allow automatic, reachability-preserving translation into differential dynamic logic, a logic for hybrid (discrete-continuous) programs. Verification is achieved by discharging the resulting formulas with the theorem prover KeYmaera X. We demonstrate the usability of our approach with case studies.
Cite as

Eduard Kamburjan, Stefan Mitsch, and Reiner Hähnle. A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 04:1-04:34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{kamburjan_et_al:LITES.8.2.4,
  author =	{Kamburjan, Eduard and Mitsch, Stefan and H\"{a}hnle, Reiner},
  title =	{{A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{04:1--04:34},
  ISSN =	{2199-2002},
  year =	{2022},
  volume =	{8},
  number =	{2},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LITES.8.2.4},
  doi =		{10.4230/LITES.8.2.4},
  annote =	{Keywords: Active Objects, Differential Dynamic Logic, Hybrid Systems}
}
Document
DOI: 10.4230/OASIcs.Gabbrielli.1
Locally Static, Globally Dynamic Session Types for Active Objects

Authors: Reiner Hähnle, Anton W. Haubner, and Eduard Kamburjan

Published in: OASIcs, Volume 86, Recent Developments in the Design and Implementation of Programming Languages (2020)

Abstract
Active object languages offer an attractive trade-off between low-level, preemptive concurrency and fully distributed actors: syntactically identifiable atomic code segments and asynchronous calls are the basis of cooperative concurrency, still permitting interleaving, but nevertheless being mechanically analyzable. The challenge is to reconcile local static analysis of atomic segments with the global scheduling constraints it depends on. Here, we propose an approximate, hybrid approach; At compile-time we perform a local static analysis: later, any run not complying to a global specification is excluded via runtime checks. That specification is expressed in a type-theoretic language inspired by session types. The approach reverses the usual (first global, then local) order of analysis and, thereby, supports analysis of open distributed systems.
Cite as

Reiner Hähnle, Anton W. Haubner, and Eduard Kamburjan. Locally Static, Globally Dynamic Session Types for Active Objects. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 1:1-1:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{hahnle_et_al:OASIcs.Gabbrielli.1,
  author =	{H\"{a}hnle, Reiner and Haubner, Anton W. and Kamburjan, Eduard},
  title =	{{Locally Static, Globally Dynamic Session Types for Active Objects}},
  booktitle =	{Recent Developments in the Design and Implementation of Programming Languages},
  pages =	{1:1--1:24},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-171-9},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{86},
  editor =	{de Boer, Frank S. and Mauro, Jacopo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.1},
  URN =		{urn:nbn:de:0030-drops-132237},
  doi =		{10.4230/OASIcs.Gabbrielli.1},
  annote =	{Keywords: Session Types, Active Objects, Runtime Verification, Static Verification}
}
  • Refine by Author
  • 3 Kamburjan, Eduard
  • 2 Hähnle, Reiner
  • 1 Giunti, Marco
  • 1 Haubner, Anton W.
  • 1 Johnsen, Einar Broch
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Logic and verification
  • 1 Computing methodologies → Distributed programming languages
  • 1 Computing methodologies → Model verification and validation
  • 1 Theory of computation → Distributed computing models
  • 1 Theory of computation → Object oriented constructs
  • Show More...

  • Refine by Keyword
  • 2 Active Objects
  • 1 Coq
  • 1 Differential Dynamic Logic
  • 1 Hybrid Systems
  • 1 Java
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 2 2023
  • 1 2020
  • 1 2022

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact