Envisage Publications 2015

2015 Publications
Please insert your publication here (please indicate also briefly to which task your publication belongs).

  • We want to provide open access to all Envisage papers, please provide a link to a preprint if your publication is not open access.
  • If you know the DOI, please provide it, too.

Conferences and Workshops.

  • Amir M. Ben-Amram and Samir Genaim. Complexity of Bradley-Manna-Sipma Lexicographic Ranking Functions. In 27th International Conference on Computer Aided Verification (CAV 2015), LNCS 9207, pp. 304-321. Springer,  2015. (T3.3)
    pointing_finger DOI: 10.1007/978-3-319-21668-3_18. Download a preprint.
  • Pierre Ganty, Samir Genaim, Ratan Lal, and Pavithra Prabhakar. From Non-Zenoness Verification to Termination. In 13th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE’15).  IEEE, 2015. (T3.3)
    pointing_finger DOI: 10.1109/MEMCOD.2015.7340490. Download a preprint.
  • Elvira Albert, Puri Arenas, Jesús Correas, Samir Genaim, Miguel Gómez-Zamalloa, Enrique Martin-Martin, Germán Puebla, and Guillermo Román-Díez. Resource Analysis: From Sequential to Concurrent and Distributed Programs. FM 2015: Formal Methods – 20th International Symposium, LNCS 9109, pp. 3-17. Springer, 2015. (T3.3)
    pointing_finger DOI: 10.1007/978-3-319-19249-9_1. Download a preprint.
  • Elvira Albert, Puri Arenas, and Miguel Gómez-Zamalloa. Test Case Generation of Actor Systems. In 13th International Symposium on Automated Technology for Verification and Analysis (ATVA 2015).  LNCS 9363, pp. 259-275. Springer, 2015. (T3.5)
    pointing_finger DOI: 10.1007/978-3-319-24953-7_21. Download a preprint.
  • Elvira Albert,  Puri Arenas, Miguel Gómez-Zamalloa, and Jose Miguel Rojas. Test Case Generation by Symbolic Execution: Basic Concepts, a CLP-Based Instance, and Actor-Based Concurrency. In: Formal Methods for Executable Software Models. LNCS 8483. Springer, 2015.
    pointing_finger DOI:     10.1007/978-3-319-07317-0_7.
  • Elvira Albert, Samir Genaim, and Pablo Gordillo. May-Happen-in-Parallel Analysis for Asynchronous Programs with Inter-Procedural Synchronization. In Static Analysis – 22nd International Symposium (SAS 2015). LNCS 9291, pp. 72-89, Springer 2015.  (T3.3)
    pointing_finger DOI: 10.1007/978-3-662-48288-9_5. Download a preprint.
  • Elvira Albert, Jesús Correas, Einar Broch Johnsen, and Guillermo Román-Díez. Parallel Cost Analysis of Distributed Systems. In Static Analysis – 22nd International Symposium (SAS 2015) . LNCS 9291, pp.  275-292. Springer, 2015.  (T3.3)
    pointing_finger DOI: 10.1007/978-3-662-48288-9_16. Download a preprint.
  • Elvira Albert, Jesús Correas, and Guillermo Román-Díez. Non-Cumulative Resource Analysis. In Proceedings of 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015), LNCS 9035, pp. 85-100. Springer, 2015. (T3.3)
    pointing_finger DOI: 10.1007/978-3-662-46681-0_6. Download a preprint.
  • E. B. Johnsen, K. I Pun, M Steffen, S. L. Tapia Tarifa and I. C. Yu. Meeting Deadlines, Elastically. In: L. Petre, E. Sekerinski (eds.):From Action Systems to Distributed Systems: the Refinement Approach. CRC Press, 2015.
    pointing_finger DOI: 10.1201/b20053-11. Download a preprint.
  • C. C. Din, R. Bubel and R. Hähnle. KeY-ABS: A deductive verification tool for the concurrent modelling language ABS. In Proceedings of the 25th International Conference on Automated Deduction (CADE 2015), LNCS. Springer, 2015.
    pointing_fingerDOI:10.1007/978-3-319-21401-6_35. Download a preprint.
  • C. C. Din, S. L. Tapia Tarifa, R. Hähnle and E. B. Johnsen. History-Based Speci fication and Veri fication of Scalable Concurrent and Distributed Systems. In Proceedings of the 17th International Conference on Formal Engineering Method (ICFEM 2015), LNCS 9407. Springer, 2015.
    pointing_finger DOI: 10.1007/978-3-319-25423-4 14. Download a preprint.
  • R. Bubel, C. C. Din, R. Hähnle and K. Nakata. A Dynamic Logic with Traces and Coinduction. In Proceedings of the 23th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux 2015), LNCS. Springer, 2015.
    pointing_finger DOI: 10.1007/978-3-319-24312-2_21. Download  a preprint.
  • S. de Gouw, J. Rot, F.S. de Boer, R. Bubel and R. Hähnle. OpenJDK’s Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case. In Proceedings of the 27th International Conference on Computer Aided Verification (CAV 2015). LNCS 9206, Springer, 2015.
    pointing_finger DOI: 10.1007/978-3-319-21690-4_16. Download a preprint.
  • S. de Gouw, M. Lienhardt, J. Mauro, B. Nobakht and Gianluigi Zavattaro. On the Integration of Automatic Deployment into the ABS Modeling Language. In Proceedings of the 4th European Conference on Service Oriented and Cloud Computing (ESOCC 2015). LNCS 9306, Springer, 2015.
    pointing_finger DOI: 10.1007/978-3-319-24072-5_4. Download a preprint.
  • B. Nobakht, S. de Gouw and F.S. de Boer. Formal Verification of Service Level Agreements Through Distributed Monitoring. In Proceedings of the 4th European Conference on Service Oriented and Cloud Computing (ESOCC 2015). LNCS 9306, Springer, 2015.
    pointing_finger DOI: 10.1007/978-3-319-24072-5_9. Download a preprint.
  • Abel Garcia, Cosimo Laneve, Michael Lienhardt: Static analysis of cloud elasticity. PPDP 2015: 125-136, ACM, 2015.
    pointing_finger DOI: 10.1145/2790449.2790524. Download a preprint.

Journals

  • Elvira Albert, Richard Bubel, Samir Genaim, Reiner Hähnle, Germán Puebla, and Guillermo Román-Díez. A Formal Verification Framework for Static Analysis. Software and Systems Modeling, 2015. To appear. 2015.
    pointing_finger DOI: 10.1007/s10270-015-0476-y. Download a preprint.
  • E. Albert, P. Arenas, J. Correas, S. Genaim, M. Gómez-Zamalloa, G. Puebla, and G. Román-Díez. Object-Sensitive Cost Analysis for Concurrent Objects. Software Testing, Verification and Reliability, 25(3):218-271, 2015. (T3.3)
    pointing_finger DOI: 10.1002/stvr.1569. Download a preprint.
  • Elvira Albert, Puri Arenas, Samir Genaim, and Germán Puebla. A Practical Comparator of Cost Functions and Its Applications. Science of Computer Programming, 2015. To appear. (T3.3)
    pointing_finger DOI: 10.1016/j.scico.2014.12.001. Download a preprint.
  • Elvira Albert, Jesús Correas, Germán Puebla, and Guillermo Román-Díez. A Multi-Domain Incremental Analysis Engine and its Application to Incremental Resource Analysis. Theoretical Computer Science,  585(0):91-114, 2015. (T3.3)
    pointing_finger DOI: 10.1016/j.tcs.2015.03.002. Download a preprint.
  • Elvira Albert, Jesús Correas, Germán Puebla, and Guillermo Román-Díez. Quantified Abstract Configurations of Distributed Systems. Formal Aspects of Computing, 27(4):665-699, 2015. (T3.3)
    pointing_finger DOI: 10.1007/s00165-014-0321-z. Download a preprint.
  • C. C. Din, and O. Owe.  Compositional Reasoning about Active Objects with Shared Futures. Formal Aspects of Computing 27(3):551-572, 2015.
    pointing_finger     DOI: 10.1007/s00165-014-0322-y. Download a preprint.
  • J. Dovland, E. B. Johnsen, O. Owe, and I. C. Yu. A Proof System for Adaptable Class Hierarchies. Journal of Logical and Algebraic Methods in Programming 84(1): 37–53.
    pointing_finger DOI: 10.1016/j.jlamp.2014.09.001. Download a preprint.
  • 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.
    pointing_finger DOI: 10.1016/j.jlamp.2014.07.001. Download a preprint.
  • V. Serbanescu, F. Pop, V. Cristea, and G. Antoniu. A formal method for rule analysis and validation in distributed data aggregation service. World Wide Web. Springer, 2015.
    pointing_finger DOI: 10.1007/s11280-015-0334-4. Download a preprint.
  • P.Y.H. Wong, R. Bubel, F.S. de Boer, M. Gómez-Zamalloa, S. de Gouw, R. Hähnle, K. Meinke and M.A. Sindhu. Testing abstract behavioral specifications. International Journal on Software Tools for Technology Transfer 17(1): 107-119, 2015.
    pointing_finger DOI: 10.1007/s10009-014-0301-x. Download a preprint.
  • Reiner Hähnle, Einar Broch Johnsen. Designing Resource-Aware Cloud Applications. IEEE Computer 48(6), 2015.  
    pointing_finger DOI: 10.1109/MC.2015.172. Download a preprint.
  • Cosimo Laneve, Luca Padovani. An algebraic theory for web service contracts. Formal Asp. Comput. 27(4): 613-640 (2015)                                                                                                 pointing_finger DOI: 10.1007/s00165-015-0334-2. Download a preprint.
  • E. Giachino, C. Laneve, and M. Lienhardt. A Framework for Deadlock Detection in ABS. Journal of Software and Systems Modeling, to appear, 2015.
    pointing_finger     DOI: 10.1007/s10270-014-0444-y. Download a preprint.