Proceedings of 14th Brazilian Symposium, SBMF 2011, Sao Paulo, September 26-30 2011

[1] Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Je.rey D. Ullman. Compilers:
Principles, Techniques, and Tools. Pearson Education, 2007.
[2] Eric Bruneton, Romain Lenglet, and Thierry Coupaye. ASM: a code manipulation
tool to implement adaptable systems. In Adaptable and Extensible
Component Systems, 2002.
[3] E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of
finite-state concurrent systems using temporal logic specifications. ACM
Transactions on Programming Languages and Systems, 8:244–263, 1996.
[4] Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization
skeletons using branching-time temporal logic. In Logic of
Programs, Workshop, pages 52–71, London, UK, 1982. Springer-Verlag.
[5] Eclipse Foundation. Eclipse website, 2009. http://www.eclipse.org.
[6] Michael D. Ernst. Type Annotations Specification (JSR 308). http://
types.cs.washington.edu/jsr308/, October 5, 2009.
[7] Michael D. Ernst, Je. H. Perkins, Philip J. Guo, Stephen McCamant, Carlos
Pacheco, Matthew S. Tschantz, and Chen Xiao. The Daikon system for
dynamic detection of likely invariants. Science of Computer Programming,
69(1–3):35–45, December 2007.
[8] David Hovemeyer and William Pugh. Finding bugs is easy. ACM SIGPLAN
Notices, 39(12):92–106, 2004.
[9] Sara Kalvala, Richard Warburton, and David Lacey. Program transformations
using temporal logic side conditions. ACM Transactions on Programming
Languages and Systems (TOPLAS), 31(4), 2009.
[10] Aditya Kanade, Amitabha Sanyal, and Uday Khedker. A PVS based framework
for validating compiler optimizations. In SEFM ’06: Proceedings of
the Fourth IEEE International Conference on Software Engineering and
Formal Methods, Washington, DC, USA, 2006. IEEE Computer Society.
[11] David Lacey. Program Transformation using Temporal Logic Specifications.
PhD thesis, Oxford University Computing Laboratory, 2003.
[12] S. Lerner, T. Millstein, and C. Chambers. Automatically proving the
correctness of compiler optimizations. In Proceedings of the ACM SIG-
PLAN 2003 conference on Programming language design and implementation.
ACM Press, 2003.
[13] Sorin Lerner, Todd Millstein, Erika Rice, and Craig Chambers. Automated
soundness proofs for dataflow analyses and transformations via local rules.
In POPL ’05: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium
on Principles of Programming Languages, pages 364–377, New York,
NY, USA, 2005. ACM Press.
[14] S. Muchnick. Advanced Compiler Design and Implementation. Morgan
Kaufmann, 1997.
[15] Martin Odersky, Lex Spoon, and Bill Venners. Programming in Scala.
Artima Press, second edition, 2010.
[16] Roopsha Samanta, Jyotirmoy V. Deshmukh, and E. Allen Emerson. Automatic
generation of local repairs for boolean programs. In FMCAD, 2008.
[17] D.A. Schmidt and B. Ste.en. Data-flow analysis as model checking of
abstract interpretations. In G. Levi, editor, 5th Static Analysis Symposium,
volume 1503 of Lecture Notes in Computer Science, September 1998.
[18] Jorg Spieler. UCDetector: the Unnecessary Code Detector website, 2007.
URL: http://www.ucdetector.org.
[19] B. Ste.en. Generating data flow analysis algorithms from modal specifications.
Science of Computer Programming, 21:115–139, 1993.
[20] Richard Warburton and Sara Kalvala. From specification to optimisation:
An architecture for optimisation of Java bytecode. In Oege de Moor and Michael I. Schwartzbach, editors, Compiler Construction, 18th International
Conference, volume 5501 of Lecture Notes in Computer Science. Springer, 2009.