**************************
Publications and workshops
**************************

This page lists ABS workshops and selected research papers on the
development and usage of the ABS modeling language and analysis tools.

ABS workshops
=============

- **2025** APM Workshop 2025: October 1-3, 2025, Porto,
  Portugal. `<https://apm-workshop.github.io/2025/>`__

- **2024** APM Workshop 2024: October 02-04, 2024, Turin,
  Italy. `<https://edkamb.github.io/APM_24/>`__

- **2023** Fifth International ABS Workshop: October 04-06, 2023,
  Lyon, France. `<https://edkamb.github.io/ABS_23/>`__

- **2021** Fourth International ABS Workshop: August 26--August 27,
  2021, Virtual.
  `<https://formbar.raillab.de/en/abs-workshop-2021/>`__

- **2019** Third International ABS Workshop: May 13--May 15, 2019,
  Amsterdam, The Netherlands.
  `<https://www.cwi.nl/research/groups/formal-methods/events/third-international-workshop-on-the-abs-modeling-language-and-tools>`__

- **2018** Second International ABS Workshop: May 28--May 30, 2018,
  Darmstadt, Germany.  `<https://formbar.raillab.de/en/abs2018/>`__

- **2017** First International ABS Workshop: May 31--June 2, 2017,
  Oslo, Norway.

Case studies
============

- | G. Turin, A. Borgarelli, S. Donetti, F. Damiani, E. B. Johnsen,
    and S. L. Tapia Tarifa.
  | *Predicting resource consumption of Kubernetes container systems
    using resource models*
  | Journal of Systems and Software, Volume 203, September 2023.
  | DOI: `10.1016/j.jss.2023.111750
    <https://doi.org/10.1016/j.jss.2023.111750>`__. Download a `preprint
    <https://ebjohnsen.org/publication/23-jss/>`__.

- | J-C Lin, M-C Lee, I. C. Yu, and E. B. Johnsen.
  | *A configurable and executable model of Spark Streaming on Apache YARN*
  | International Journal of Grid and Utility Computing. Volume 11(2). Indescience, 2020.
  | DOI: `10.1504/IJGUC.2020.105531 <https://doi.org/10.1504/IJGUC.2020.105531>`__. Download a `preprint <https://ebjohnsen.org/publication/20-ijguc/20-ijguc.pdf>`__.

- | E. Kamburjan, R. Hähnle, and S. Schön
  | *Formal modeling and analysis of railway operations with active objects*
  | Science of Computer Programming. Volume 166. Elsevier, 2018.
  | DOI: `10.1016/j.scico.2018.07.001 <https://doi.org/10.1016/j.scico.2018.07.001>`__.

- | E. Albert, F. de Boer, R. Hähnle, E. B. Johnsen, R. Schlatte, S. L. Tapia Tarifa, and P. Y. H. Wong.
  | *Formal modeling and analysis of resource management for cloud architectures: an industrial case study using Real-Time ABS*
  | Service Oriented Computing and Applications 8 (4):323-339, 2014.
  | DOI: `10.1007/s11761-013-0148-0 <http://dx.doi.org/10.1007/s11761-013-0148-0>`__. Download a `preprint <https://ebjohnsen.org/publication/14-soca/14-soca.pdf>`__.


Language development
====================

- | L. Tveito, E. B. Johnsen, and R. Schlatte.
  | *Global Reproducibility through Local Control for Distributed Active Objects*
  | In Proc. 23th International Conference on Fundamental Approaches to Software Engineering (FASE 2020), LNCS 12076. Springer , 2020.
  | DOI: `10.1007/978-3-030-45234-6_7 <https://doi.org/10.1007/978-3-030-45234-6_7>`__. Download a `preprint <https://ebjohnsen.org/publication/20-fase/20-fase.pdf>`__.

- | R. Schlatte, E. B. Johnsen, J. Mauro, S. L. Tapia Tarifa, and I. C. Yu.
  | *Release the Beasts: When Formal Methods Meet Real World Data*
  | Festschrift Farhad Arbab, LNCS 10865. Springer , 2018.
  | DOI: `10.1007/978-3-642-25271-6_8 <http://dx.doi.org/10.1007/978-3-642-25271-6_8>`__. Download a `preprint <https://ebjohnsen.org/publication/18-farhad/18-farhad.pdf>`__.

- | E. Kamburjan.
  | *From post-conditions to post-region invariants: deductive verification of hybrid objects*
  | In 24th ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2021). ACM , 2021.
  | DOI: `10.1145/3447928.3456633 <https://doi.org/10.1145/3447928.3456633>`__.

- | E. B. Johnsen, R. Hähnle, J. Schäfer, R. Schlatte, and M. Steffen.
  | *ABS: A Core Language for Abstract Behavioral Specification*
  | In Proc. 9th Intl. Symp. on Formal Methods for Components and Objects (FMCO 2010), LNCS 6957. Springer , 2011.
  | DOI: `10.1007/978-3-642-25271-6_8 <http://dx.doi.org/10.1007/978-3-642-25271-6_8>`__. Download a `preprint <https://ebjohnsen.org/publication/10-fmco/10-fmco.pdf>`__.

- | E. B. Johnsen, R. Schlatte, and S. L. Tapia Tarifa.
  | *Integrating Deployment Architecture and Resource Consumption in Timed Object-Oriented Models*
  | Journal of Logical and Algebraic Methods in Programming 84(1): 67-91, 2015.
  | DOI: `10.1016/j.jlamp.2014.07.001 <http://dx.doi.org/10.1016/j.jlamp.2014.07.001>`__.  Download a `preprint <https://ebjohnsen.org/publication/15-jlamp1/15-jlamp1.pdf>`__.

- | Joakim Bjørk, Frank S. de Boer, Einar Broch Johnsen, Rudolf Schlatte, and S. L. Tapia Tarifa.
  | *User-defined schedulers for real-time concurrent objects*
  | Innovations Syst Softw Eng 9(1): 29-43 (2013).
  | DOI: `10.1007/s11334-012-0184-5 <https://doi.org/10.1007/s11334-012-0184-5>`__.  Download a `preprint <https://ebjohnsen.org/publication/13-isse/13-isse.pdf>`__.

- | F. Damiani, R. Hähnle, E. Kamburjan, M. Lienhardt.
  | *A Unified and Formal Programming Model for Deltas and Traits*
  | Proc. 20th International Conference on Fundamental Approaches to Software Engineering (FASE 2017), LNCS 10202. Springer, 2017.
  | DOI: `10.1007/978-3-662-54494-5_25 <https://doi.org/10.1007/978-3-662-54494-5_25>`__.  Download a [postprint <http://hdl.handle.net/2318/1633390>`__.

Software product lines
======================


- | F. Damiani, R. Hähnle, E. Kamburjan, M. Lienhardt, and L. Paolini.
  | *Variability modules*
  | Journal of Systems and Software, Volume 195, January 2023.
  | DOI: `10.1016/j.jss.2022.111510 <https://doi.org/10.1016/j.jss.2022.111510>`__.

- | F. Damiani, M. Lienhardt, R. Muschevici, I. Schaefer.
  | *An Extension of the ABS Toolchain with a Mechanism for Type Checking SPLs*
  | Proc. 13th International Conference on Integrated Formal Methods (IFM 2017), LNCS 10510. Springer, 2017.
  | DOI: `10.1007/978-3-319-66845-1_8 <https://doi.org/10.1007/978-3-319-66845-1_8>`__.  Download a [postprint <http://hdl.handle.net/2318/1649744>`__.

Deductive verification
======================

- | E. Kamburjan, C. C. Din, R. Hähnle and E. B. Johnsen.
  | *Behavioral Contracts for Cooperative Scheduling*
  | In  Deductive Software Verification: Future Perspectives, LNCS 12345. Springer, 2020.
  | DOI: `10.1007/978-3-030-64354-6_4 <https://doi.org/10.1007/978-3-030-64354-6_4>`__. Download a `preprint <https://ebjohnsen.org/publication/20-key2/20-key2.pdf>`__.

- | C. C. Din, R. Bubel and R. Hähnle.
  | *KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS*
  | In Proc. 25th Intl. Conf. on Automated Deduction (CADE 2015), LNCS 9195. Springer, 2015.
  | DOI:[10.1007/978-3-319-21401-6_35 <http://doi.org/10.1007/978-3-319-21401-6_35>`__. Download a `preprint <http://envisage-project.eu/wp-content/uploads/2014/12/KeYABS-CADE15.pdf>`__.

- | C. C. Din, S. L. Tapia Tarifa, R. Hähnle and E. B. Johnsen.
  | *History-Based Specification and Verification of Scalable Concurrent and Distributed Systems*
  | In Proc. 17th Intl. Conf. on Formal Engineering Method (ICFEM 2015), LNCS 9407. Springer, 2015.
  | DOI: `10.1007/978-3-319-25423-4_14 <http://doi.org/10.1007/978-3-319-25423-4_14>`__. Download a `preprint <http://envisage-project.eu/wp-content/uploads/2014/12/ICFEM_2015_submission_59.pdf>`__.

Analysis
========

- | C. Laneve, M. Lienhardt, K. I Pun, and G. Román-Díez.
  | *Time analysis of actor programs*
  | Journal of Logical and Algebraic Methods in Programming, Volume 105, Elsevier, 2019.
  | DOI: `10.1016/j.jlamp.2019.02.007 <https://doi.org/10.1016/j.jlamp.2019.02.007>`__.

- | A. Garcia, C. Laneve, and M. Lienhardt.
  | *Static analysis of cloud elasticity*
  | Science of Computer Programming, Volume 147, Elsevier, 2017.
  | DOI: `10.1016/j.scico.2017.03.008 <https://doi.org/10.1016/j.scico.2017.03.008>`__.

- | E. Albert, P. Arenas, A. Flores-Montoya, S. Genaim, M. Gómez-Zamalloa, E. Martin-Martin, G. Puebla, and G. Román-Díez.
  | *SACO: Static Analyzer for Concurrent Objects*
  | In Proc. 20th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS 8413, Springer, 2014.
  | DOI: `10.1007/978-3-642-54862-8_46 <http://dx.doi.org/10.1007/978-3-642-54862-8_46>`__. Download a `preprint <http://eprints.ucm.es/36623/1/SACO%20static%20analyzer%20for%20concurrent.pdf>`__.

- | E. Giachino, C. Laneve, and M. Lienhardt.
  | *A Framework for Deadlock Detection in ABS*
  | Journal of Software and Systems Modeling, Volume 15(4), Springer, 2015.
  | DOI: `10.1007/s10270-014-0444-y <http://dx.doi.org/10.1007/s10270-014-0444-y>`__.

ABS tools
=========

- | Rudolf Schlatte, Einar Broch Johnsen, Eduard Kamburjan and S. Lizeth Tapia Tarifa
  | *The ABS simulator toolchain*
  | Science of Computer Programming. Volume 233. Elsevier, 2022.
  | DOI: `10.1016/j.scico.2022.102861 <https://doi.org/10.1016/j.scico.2022.102861>`__.

Code generation from ABS
========================

- | B. Nobakht and F. S. de Boer.
  | *Programming with Actors in Java 8*
  | In Proc. of the 6th Intl. Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA’14). LNCS 8803. Springer, 2014.
  | DOI: `10.1007/978-3-662-45231-8_4 <http://dx.doi.org/10.1007/978-3-662-45231-8_4>`__. Download a `preprint <http://envisage-project.eu/wp-content/uploads/2015/02/paper-j8-isola.pdf>`__.

Model-based deployment and monitoring
=====================================

- | R. Hähnle and E. B. Johnsen.
  | *Designing Resource-Aware Cloud Applications*
  | IEEE Computer 48 (6), 2015.
  | DOI: `10.1109/MC.2015.172 <http://doi.ieeecomputersociety.org/10.1109/MC.2015.172>`__. Download a `preprint <http://envisage-project.eu/wp-content/uploads/2013/09/ResourceAwareApplicationsForTheCloud_Preprint.pdf>`__.

- | B. Nobakht, S. de Gouw and F.S. de Boer.
  | *Formal Verification of Service Level Agreements Through Distributed Monitoring*
  | In Proc. 4th European Conf. on Service Oriented and Cloud Computing (ESOCC 2015). LNCS 9306, Springer, 2015.
  | DOI: `10.1007/978-3-319-24072-5_9 <http://dx.doi.org/10.1007/978-3-319-24072-5_9>`__. Download a `preprint <http://envisage-project.eu/wp-content/uploads/2015/09/paper-esocc.pdf>`__.