Envisage Publications 2014

2014 Publications

Conferences and Workshops.

  • 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.
    pointing_finger     DOI: 10.1007/978-3-642-54862-8_46. Download a preprint.
  • E. Albert, P. Arenas, and M. Gómez-Zamalloa. Actor- and Task-Selection Strategies for Pruning Redundant State-Exploration in Testing. In Proc. Formal Techniques for Distributed Objects, Components and Systems (FORTE 2014), LNCS 8461, pp 49–65. Springer, 2014.
    pointing_finger     DOI: 10.1007/978-3-662-43613-4_4. Download a preprint.
  • E. Albert, P. Arenas, M. Gómez-Zamalloa, and J. M. Rojas. Test Case Generation by Symbolic Execution: Basic Concepts, a CLP-Based Instance, and Actor-Based Concurrency. In Proc. of SFM’14: ESM, LNCS 8483, pp 263–309. Springer, 2014.
    pointing_finger     DOI: 10.1007/978-3-319-07317-0_7. Download a preprint.
  • E. Albert, J. Correas, E. Martín-Martín, and G. Román-Díez. Static Inference of Transmission Data Sizes in Distributed Systems. In Proc. of the 6th Intl. Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA’14). LNCS 8803, pp 106-121. Springer, 2014.
    pointing_finger     DOI: 10.1007/978-3-662-45231-8_8. Download a preprint.
  • E. Albert, J. Correas, and G. Román-Díez. Peak Cost Analysis of Distributed Systems. In Proc. 21st International Static Analysis Symposium (SAS’14), LNCS 8723, pp  18–33. Springer, 2014.
    pointing_finger     DOI: 10.1007/978-3-319-10936-7_2. Download a preprint.
  • F. S. de Boer and S. de Gouw. Combining monitoring with run-time assertion checking. In Proc. of SFM’14: ESM, LNCS 8483, pp 217–262. Springer, 2014.
    pointing_finger     DOI: 10.1007/978-3-319-07317-0_6. Download a preprint.
  • R. Bubel, R. Hähnle, and M. Pelevina. Fully abstract operation contracts. In Proc. of the 6th Intl. Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA’14). LNCS 8803, pp 122–136. Springer, 2014.
    pointing_finger     DOI: 10.1007/978-3-662-45231-8_9. Download a preprint.
  • R. Bubel, A. F. Montoya, and R. Hähnle. Analysis of executable software models. In Proc. of SFM’14:ESM, LNCS 8483, pp 1–27. Springer, 2014.
    pointing_finger     DOI: 10.1007/978-3-319-07317-0_1. Download a preprint.
  • C. C. Din, O. Owe and R. Bubel. Runtime Assertion Checking and Theorem Proving for Concurrent and Distributed Systems. Proc. MODELSWARD’14. SCITEPRESS 2014.
    pointing_finger     DOI: 10.5220/0004877804800487. Download a preprint.
  • A. F. Montoya and R. Hähnle. Resource analysis of complex programs with cost equations. In Proc. 12th Asian Symposium on Programming Languages and Systems (APLAS’14), LNCS 8858, pp 275–295. Springer, 2014.
    pointing_finger     DOI: 10.1007/978-3-319-12736-1_15. Download a preprint.
  • E. Giachino, N. Kobayashi, and C. Laneve. Deadlock analysis of unbounded process networks. In Proc. of CONCUR’14. LNCS 8704, pp 63-77, Springer, 2014.
    pointing_finger     DOI: 10.1007/978-3-662-44584-6_6. Download a preprint.
  • E. Giachino, and C. Laneve. Deadlock detection in linear recursive programs. In Proc. of SFM’14:ESM. LNCS 8483, pp. 26–64, Springer, 2014. 
    pointing_finger     DOI: 10.1007/978-3-319-07317-0_2. Download a preprint.
  • E. Giachino, and C. Laneve. Towards the typing of resource deployment. In Proc. of the 6th Intl. Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA’14). LNCS 8803, pp 90-105. Springer, 2014.
    pointing_finger     DOI: 10.1007/978-3-662-45231-8_7. Download a preprint.
  • G. Göri, E. B. Johnsen, R. Schlatte, and V. Stolz. Erlang-style error recovery for concurrent objects with cooperative scheduling. In Proc. of the 6th Intl. Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA’14). LNCS 8803, pp 6-22. Springer, 2014.
    pointing_finger     DOI: 10.1007/978-3-662-45231-8_2. Download a preprint.
  • R. Hähnle. Managing change in formal software analysis: Two research challenges. In Proc. of the 6th Intl. Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA’14). LNCS 8803, pp 509–511. Springer, 2014.
    pointing_finger     Download a preprint.
  • R. Hähnle and E. B. Johnsen. Introduction to track on engineering virtualized services. In Proc. of the 6th Intl. Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA’14). LNCS 8803, pp 1–4. Springer, 2014.
    pointing_finger     DOI: 10.1007/978-3-662-45231-8_1. Download a preprint.
  • E. B. Johnsen, R. Schlatte, and S. L. Tapia Tarifa. Deployment variability in delta- oriented models. In Proc. of the 6th Intl. Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA’14). LNCS 8803, pp 286–301. Springer, 2014.
    pointing_finger     DOI: 10.1007/978-3-662-45234-9_22. Download a preprint.
  • E. Kristiansen and V. Stolz. Search-based composed refactorings. In Proc. Norsk Informatikkonferanse (NIK 2014), 2014.
    pointing_finger     Permalink: ojs.bibsys.no/index.php/NIK/article/view/14. Download a preprint.
  • I. Lanese, M. Lienhardt, M. Bravetti, E. B. Johnsen, R. Schlatte, V. Stolz, and G. Zavattaro. Fault model design space for cooperative concurrency. In Proc. of the 6th Intl. Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA’14). LNCS 8803, pp 23–37. Springer, 2014.
    pointing_finger     DOI: 10.1007/978-3-662-45231-8_3. Download a preprint.
  • 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.
    pointing_finger     DOI: 10.1007/978-3-662-45231-8_4. Download a preprint.
  • O. Owe and I. C. Yu. Deadlock detection of active objects with synchronous and asynchronous method calls. In Proc. Norsk Informatikkonferanse (NIK 2014), 2014.
    pointing_finger     Permalink: ojs.bibsys.no/index.php/NIK/article/view/19. Download a preprint.
  • K. I Pun, M. Steffen, and V. Stolz. Behaviour inference for deadlock checking. In Proc. 8th Intl. Symp. on Theoretical Aspects of Software Engineering (TASE’14). IEEE Press, 2014.
    pointing_finger     DOI: 10.1109/TASE.2014.23. Download a preprint.
  • K. I Pun, M. Steffen, and V. Stolz. Effect-polymorphic behaviour inference for deadlock checking. In Proc. SEFM’14, LNCS 8702, pp 50-64. Springer, 2014.
    pointing_finger     DOI: 10.1007/978-3-319-10431-7_5. Download a preprint.
  • V. Serbanescu, F. Pop, V. Cristea, and G. Antoniu. Architecture of Distributed Data Aggregation Service. Proc. 28th International Conference on Advanced Information Networking and Applications (AINA 2014). IEEE CS Press, 2014.
    pointing_finger     DOI: 10.1109/AINA.2014.89.
  • V. Serbanescu, C. Nagarajagowda, K. Azadbakht, F. de Boer, Frank, and B. Nobakht. Towards Type-Based Optimizations in Distributed Applications Using ABS and JAVA 8. Adaptive Resource Management and Scheduling for Cloud Computing. LNCS 8907, pp. 103–112. Springer 2014.
    pointing_finger     DOI: 10.1007/978-3-319-13464-2_8.

Journals.

  • E. Albert, P. Arenas, S. Genaim, G. Puebla, and G. Román-Díez. Conditional Termination of Loops over Heap-allocated Data. Science of Computer Programming, 92:2 – 24, 2014.
    pointing_finger     DOI: 10.1016/j.scico.2013.04.006. Download a preprint.
  • E. Albert, F. de Boer, R. Hähnle, E. B. Johnsen, R. Schlatte, S. L. Tapia Tarifa, 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. (T4.3)
    pointing_finger DOI: 10.1007/s11761-013-0148-0. Download a     preprint.
  • A. M. Ben-Amram and S. Genaim. Ranking Functions for Linear-Constraint Loops. Journal of the ACM, 61(4):26, 2014.
    pointing_finger    DOI: 10.1145/2629488. Download a preprint.
  • F. S. de Boer, M. M. Jaghoori, C. Laneve, G. Zavattaro. Decidability Problems for Actor Systems. Logical Methods in Computer Science 10 (4:5)
    pointing_finger     DOI: 10.2168/LMCS-10(4:5)2014. Download a preprint.
  • C. C. Din and O. Owe.  A Sound and Complete Reasoning System for Asynchronous Communication with Shared Futures. Journal of Logical and Algebraic Methods in Programming, 2014.
    pointing_finger     DOI: 10.1016/j.jlamp.2014.03.003. Download a preprint.
  • R. Hähnle and E. B. Johnsen. Resource-aware applications for the cloud. IEEE Computer, to appear, 2014.
    pointing_finger DOI: 10.1109/MC.2015.172.     Download a preprint.
  • E. B. Johnsen, O. Owe, D. Clarke, and J. Bjørk. A formal model of service-oriented dynamic object groups. Science of Computer Programming, 201.
    pointing_finger     DOI: 10.1016/j.scico.2014.11.014. Download a preprint.
  • K. I Pun, M. Steffen, and V. Stolz. Deadlock checking by data race detection. Journal of Logical and Algebraic Methods in Programming, 2014.
    pointing_finger     DOI: 10.1016/j.jlamp.2014.07.003. 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. Software Tools for Technology Transfer,  2014.
    pointing_finger     DOI: 10.1007/s10009-014-0301-x  Download a preprint.
  • D. Zanardini and S. Genaim. Inference of Field-Sensitive Reachability and Cyclicity. ACM Transactions Computational Logic, 2014.
    pointing_finger     DOI: 10.1145/2629478. Download a preprint.

Books.

  • M. Bernardo, F. Damiani, R. Hähnle, E. B. Johnsen, and I. Schaefer, editors. Executable Software Models: 14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, Bertinoro, Italy, LNCS 8483, Springer, 2014.
    pointing_finger     DOI: 10.1007/978-3-319-07317-0