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)
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)
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)
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)
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.
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)
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)
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)
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.
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.
DOI: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 Specification and Verification of Scalable Concurrent and Distributed Systems. In Proceedings of the 17th International Conference on Formal Engineering Method (ICFEM 2015), LNCS 9407. Springer, 2015.
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.
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.
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.
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.
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.
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.
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)
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)
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)
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)
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.
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.
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.
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.
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.
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.
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) 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.
DOI: 10.1007/s10270-014-0444-y. Download a preprint.