Please insert your publication here (please indicate also briefly to which task your publication belongs).
If you know the DOI, please provide it, too.

• E. Albert, I. Cabañas, A. Flores-Montoya, M. Gómez-Zamalloa, S. Gutiérrez. jPET: an Automatic Test-Case Generator for Java. 18th Working Conference on Reverse Engineering (WCRE 2011), pages 441--442,  IEEE Computer Society. Limerick, Ireland, October 2011 (T 2.3) [DOI: 10.1109/WCRE.2011.67]
• E. Albert, M. Gómez-Zamalloa, J.M. Rojas. Towards Resource-driven CLP-based Test Case Generation. 21th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2011), July 2011. Extended Abstract (T 2.3)
• E. Albert, P. Arenas, S. Genaim,  M.  Gómez-Zamalloa, G. Puebla. Cost Analysis of Concurrent OO Programs. Ninth Asian Symposium on Programming Languages and Systems (APLAS 2011), volume 7078 of Lecture Notes in Computer Science, pages 238--254, Springer. Kenting, Taiwan, December 5-7, 2011  (T 4.2) [DOI: 10.1007/978-3-642-25318-8_19]
• E. Albert, P. Arenas, S. Genaim, D. Zanardini. Task-Level Analysis for a Language with Async-Finish Parallelism. ACM SIGPLAN/SIGBED Conference on Languages, Compilers, Tools and Theory for Embedded Systems (LCTES 2011), ACM Press. Chicago, IL, USA, April 2011,  (T 4.2) [DOI: 10.1145/1967677.1967681] 
• E. Albert, Samir Genaim, Abu Naser Masud. More Precise yet Widely Applicable Cost Analysis. Verification, Model Checking, and Abstract Interpretation, 12th International Conference (VMCAI 2011), volume 6538 of Lecture Notes in Computer Science, pages 38-53, Springer. Austin, TX, USA, January 2011,  (T 4.2) [DOI: 10.1007/978-3-642-18275-4_5]
• E. Albert, R. Bubel, S. Genaim, R. Hähnle, G. Puebla, G. Román-Díez. Verified Resource Guarantees using COSTA and KeY. Proceedings of the 2011 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2011), pages 73-76, ACM. Austin, TX, USA, April 2011, (T 4.2) [DOI: 10.1145/1929501.1929513]
• E. Albert, S. Genaim, M.  Gómez-Zamalloa, E. B. Johnsen, R. Schlatte, S. L. Tapia Tarifa. Simulating Concurrent Behaviors with Worst-Case Cost Bounds. 17th Interational Symposium on Formal Methods (FM 2011), volume 6664 of Lecture Notes in Computer Science, pages 353-368, Springer. Lero, Limerick, Ireland, June 2011. (T2.1) [DOI: 10.1007/978-3-642-21437/0_27]
• D. Alonso, P. Arenas, S. Genaim. Handling Non-Linear Operations in the Value Analysis of COSTA. 6th Workshop on Bytecode Semantics, verification, Analysis and Transformation. Saarbrucken, Germany, March 2011. Electronic Notes in Theoretical Computer Science 279(1):3-17,  Elsevier, (T5.3) [DOI: 10.1016/j.entcs.2011.11.002]
• E. B. Johnsen, O. Owe, R. Schlatte, and S. L. Tapia Tarifa. Validating Timed Models of Deployment Components with Parametric Concurrency. Proceedings of the International Conference on Formal Verification of Object-Oriented Software (FoVeOOS’10), volume 6528 of Lecture Notes in Computer Science, pages 46–60. Springer-Verlag, 2011. (T2.1) [DOI: 10.1007/978-3-642-18070-5_4]
• R. Schlatte, E. B. Johnsen, F. Kazemeyni, and S. L. Tapia Tarifa. Models of Rate Restricted Communication for Concurrent Objects. Proceedings of the 4th International Workshop on Harnessing Theories for Tool Support in Software (TTSS’10), Electronic Notes in Theoretical Computer Science 274:67-81. Elsevier, 2011.  (T2.1) [DOI: 10.1016/j.entcs.2011.07.007]
• I. Schaefer, L. Bettini, F. Damiani. Compositional Type-Checking for Delta-oriented Programming. Intl. Conference on Aspect-oriented Software Development (AOSD'11), Porto de Galinihas, Brasil, March 21-25, 2011. (T2.3)
• R. Muschevici, J. Proenca, D. Clarke. Modular Modelling of Software Product Lines with Feature Nets. In: Software Engineering and Formal Methods (SEFM), LNCS, Springer-Verlag, 2011. (T1.2, T2.2)
• Y. Welsch, J. Schäfer. Location Types for Safe Distributed Object-Oriented Programming. In: 49th International Conference on Objects, Models, Components and Patterns (TOOLS Europe 2011). LNCS, volume 6705, Springer, p. 194-210, June, 2011 (T1.3) [DOI:10.1007/978-3-642-21952-8_15]
• Y. Welsch, A. Poetzsch-Heffter. Full Abstraction at Package Boundaries of Object-Oriented Languages. In: Formal Methods, Foundations and Applications (SBMF 2011). LNCS, volume 7021, Springer, p. 28-43, 2011 (T3.1, T2.6) [DOI:10.1007/978-3-642-25032-3_3]
• M. Lienhardt, I. Lanese, M. Bravetti, D. Sangiorgi, G. Zavattaro, Y. Welsch, J. Schäfer, A. Poetzsch-Heffter. A Component Model for the ABS Language. In: Aichernig, B., de Boer, F., Bonsangue, M. (eds.) Formal Methods for Components and Objects (FMCO 2010). LNCS, vol. 6957. Springer, 2011 (T3.1)
• Elena Giachino, Cosimo Laneve. Analysis of Deadlocks in Object Groups. FMOODS/FORTE 2011. Springer LNCS 6722, pp. 168-182 (T2.5, T4.3)
• Einar Broch Johnsen, Ivan Lanese, Gianluigi Zavattaro: Fault in the Future. COORDINATION 2011: 1-15 (T2.1) [DOI: 10.1007/978-3-642-21464-6_1]
• Mario Bravetti, Cinzia Di Giusto, Jorge A. Pérez, Gianluigi Zavattaro. Adaptable Processes (Extended Abstract). FMOODS/FORTE 2011. Springer LNCS 6722, pp. 90-105. (T3.1, T3.3)
• D. Clarke, R. Muschevici, J Proenca, I . Schaefer, R. Schlatte. Variability modelling in the ABS language. In: Aichernig, B., de Boer, F., Bonsangue, M. (eds.) Formal Methods for Components and Objects (FMCO 2010). LNCS, vol. 6957. Springer, 2011 (T1.2)
• E. B. Johnsen, R. Hähnle, J. Schäfer, R. Schlatte, M. Steffen. ABS: A Core Language for Abstract Behavioral Specification. In: Aichernig, B., de Boer, F., Bonsangue, M. (eds.) Formal Methods for Components and Objects (FMCO 2010). LNCS, vol. 6957. Springer, 2011 (T1.1) [DOI: 10.1007/978-3-642-25271-6_8]
• F. Damiani, J. Dovland, E. B. Johnsen, I. Schaefer. Verifying Traits: A Proof System for Fine-Grained Reuse. In Proc 13th Workshop on Formal Techniques for Java-like Programs (FTfJP'11). ACM Digital Library. (T 4.3). [DOI: 10.1145/2076674.2076682]
• D. Bavides, M. Leuker, M. Becker, R. Rabiser, K. Villela and P. Y. H. Wong. Formal Methods and Analysis in Software Product Line Engineering. In Proc 15th International Conference on Software Product Line Conference (SPLC 2011), Munich, Germany, IEEE Computer Society, August 2011. (T 6.1) [DOI: 10.1109/SPLC.2011.39]
• M. Helvensteijn, R. Muschevici and P. Y. H. Wong. Delta Modeling in Practice - A Fredhopper Case Study. Proc. 6th International Workshop on Variability Modelling of Software-Intensive Systems (VaMoS 2012), ACM 2012 (T5.3)
• Richard Bubel, Reiner Hähnle and Ran Ji. Program Specialization Via a Software Verification Tool. Post Conf. Proc. 9th International Symposium on Formal Methods for Components and Objects (FMCO 2010), 2011,  LNCS, Springer-Verlag (T3.4, T2.6)
• Mohammad Mahdi Jaghoori: From nonpreemptive to preemptive scheduling: from single-processor to multi-processor. Proceedings of the 2011 ACM Symposium on Applied Computing (SAC'11), p. 717-722, ACM, 2011 (T 2.1)
• E. Albert, M.Gomez-Zamalloa, J.M. Rojas, G. Puebla: Compositional CLP-based Test Data Generation for Imperative Languages. LOPSTR 2010 Revised Selected Papers, LNCS, volume 6564, Springer, 2011 (T 2.3)
• K. Meinke and F. Niu: Learning-Based Testing for Reactive Systems using Term Rewriting Technology. Proc. 23rd IFIP Int. Conf. on Testing Software and Systems (ICTSS 2011), LNCS, volume 7019, p. 97-114, Springer, 2011
• K. Meinke and M. Sindhu: Incremental Learning-based Testing for Reactive Systems. Proc Fifth Int. Conf. on Tests and Proofs (TAP2011), LNCS, volume 6707, p. 134-151, Springer, 2011
• K. Nakata: Resumption-based big-step and small-step interpreters for While with interactive I/O. Domain-Specific Languages (DSL 2011), EPTCS, volume 66, p. 226-235, Open Publishing Assoc., 2011. [ DOI: 10.4204/eptcs.66.12 ] (T4.3)
• H. Im, K. Nakata, J. Garrigue, S. Park. A syntactic type system for recursive modules. In Proc. of 2011 ACM Int. Conf. on Object-Oriented Programming, Systems, Languages and Applications, OOPSLA 2011 (Portland, OR, Oct. 2011), pp. 993-1012. ACM Press, 2011. [ DOI: 10.1145/2048066.2048141 ] (T2.4)
• P. Laud. Implementing cryptographic primitives in the symbolic model. In M. Bobaru, K. Havelund, G. J. Holzmann, R. Joshi, eds., Proc. of 3rd NASA Formal Methods Symp., NFM 2011 (Pasadena, CA, Apr. 2011), LNCS,  v. 6617, pp. 267-281. Springer, 2011. [ DOI: 10.1007/978-3-642-20398-5_20 ] (T4.1)
• M. Balliu, M. Dam, G. Le Guernic: Epistemic Temporal Logic for Information Flow Security. Proc. W. Programming Languages and Analysis for Security, 2011 (T 4.1)
• Ina Schaefer, Dilian Gurov, and Siavash Soleimanifard. Compositional Algorithmic Verification of Software Product Lines. FMCO'10 Lecture Notes in Computer Science, vol. 6957 (T 2.5)
• Siavash Soleimanifard, Dilian Gurov, and Marieke Huisman. ProMoVer: Modular Verification of Temporal Safety Properties. SEFM'11 Lecture Notes in Computer Science, vol. 7041 (T 2.5) [DOI: 10.1007/978-3-642-24690-6_25]
• Gilles Barthe, Juan Manuel Crespo, and César Kunz. Relational Verification Using Product Programs. FM 2011: 200-214. [ DOI: 10.1007/978-3-642-21437-0_17 ] (T 4.3)
• Juan Manuel Crespo, César Kunz: A Machine-Checked Framework for Relational Separation Logic. SEFM 2011: 122-137. [ DOI: 10.1007/978-3-642-24690-6_10 ](T 4.3)
• Mario Bravetti, Cinzia Di Giusto, Jorge A. Perez, Gianluigi Zavattaro: Steps on the Road to Component Evolvability. Formal Aspects of Component Software (FACS 2010). LNCS, volume 6921, Springer, p. 295-299, 2011 (T3.1)

Journals

• E. Albert, P. Arenas, S. Genaim, G. Puebla: Closed-Form Upper Bounds in Static Cost Analysis. Journal of Automated Reasoning 46 (2):161-203, Springer, 2011  (T 4.2) [DOI: 10.1007/s10817-010-9174-1]
• G. Puebla, E. Albert, M. Hermenegildo: Efficient Local Unfolding with Ancestor Stacks. Theory and Practice of Logic Programming 11 (1):1--32, Cambridge University Press, 2011 (T 2.3) [DOI:10.1017/S1471068409990263]
• I. Schaefer, R. Hähnle: Formal Methods in Software Product Line Engineering. IEEE Computer, February 2011
  
• Gilles Barthe, Exequiel Rivas: Static enforcement of information flow policies for a concurrent JVM-like language. TGC, 2011 (T 4.1)
• Gilles Barthe, Pedro D'Argenio, Tamara Rezk: Secure Information Flow by Self-Composition. Mathematical Structures in Computer Science, 2011 (T 4.1)
• M. Dam, B. Jacobs, A. Lundblad, F. Piessens: Security Monitor Inlining and Certification for Multithreaded Java. Mathematical Structures in Computer Science, 2011 (T 3.4)
• J. Dovland, E. B. Johnsen, O. Owe, and M. Steffen: Incremental Reasoning with Lazy Behavioral Subtyping for Multiple Inheritence, Science of Computer Programming, 2011 (T 2.5)

Book Chapters

• D. Clarke, N. Diakov, R. Hähnle, E. B. Johnsen, I. Schaefer, J. Schäfer, R. Schlatte, P. Y. H. Wong: Modeling Spatial and Temporal Variability with the HATS Abstract Behavioral Modeling Language. Formal Methods for Eternal Networked Software Systems; M. Bernardo, V. Issarny (eds.), Springer, 2011. (T 6.1) [DOI: 10.1007/978-3-642-21455-4_13]

Invited Talks

• P. Y. H. Wong: Modelling Distributed Adaptable Object Oriented Systems using HATS Approach: A Fredhopper Case Study, 2nd International Conference on Formal Verification of Object-Oriented Software, Torino, Italy, 2011 (T 6.1)
• D Clarke: Modelling Software Product Lines with the HATS Abstract Behavioural Modelling Language SEFM School 2011, the 9th International Conference on Software Engineering and Formal Methods, November 7-11, Montevideo, Uruguay, 2011 (T 6.1)
• D. Gurov: Modular Verification of Temporal Safety Properties of Procedural Programs. SEFM Tutorial 2011, the 9th International Conference on Software Engineering and Formal Methods, November 15-16, Montevideo, Uruguay, 2011 (T 2.5)
• T. Uustalu. Practicing Coinduction: Big-Step Semantics and Hoare Logics for Nontermination. SEFM School 2011, the 9th International Conference on Software Engineering and Formal Methods, November 7-11, Montevideo, Uruguay, 2011
• R. Hähnle: HATS: Highly Adaptable and Trustworthy Software Using Formal Models, SAP Research, Darmstadt, 18 Nov 2011 (T 6.1)
• R. Hähnle: HATS: Highly Adaptable and Trustworthy Software Using Formal Models, University of Genova, Italy, 3 October 2011 (T 6.1)