I recently had the pleasure to host a PC Meeting conference call with skype, with 22 people! Actually things went surprisingly well. However, it really helps if people stick to a few rules. I have written down a few tricks that I learned on the way.
Hosting a Program Committee meeting with Skype
Eric | August 30, 2010Soot is now invokedynamic-ready
Eric | August 24, 2010As many of you may know, JDK 7 will bring support for a new bytecode called invokedynamic. Thanks to Matthias Perner, a bright student of ours, Soot is already ready for this new bytecode today. I have just committed appropriate changes to the SVN trunk. The new instructions are handled as follows:
- On the Jimple, Grimp and Baf level, invokedynamic instructions appear as DynamicInvokeExpr with a static SootMethodRef that has class java.dyn.InvokeDynamic as target class. This is in accordance with the internal handling in JDK 7.
- SootMethodRefs which have java.dyn.InvokeDynamic as target class may not be resolved: calling resolve() will throw an exception
- On the Jasmin level, invokedynamic instruction appear in the form “invokedynamic <methodName>(<methodParams>)<methodRetType>“. In particular, there is no target class given.
- Jasmin translates this into an invokedynamic instruction with two arguments:
- a NameAndType attribute referring to <methodName>(<methodParams>)<methodRetType> and
- the constant “0” (two zero bytes, i.e., a short); according to the VM spec this is reserved for future use.
The above is an experimental design. Comments are welcome! In the near future we plan to extend TamiFlex to handle invokedynamic as well.
Clara: a Framework for Partially Evaluating Finite-state Runtime Monitors Ahead of Time
Eric | August 19, 2010In my publications section you can now find our RV 2010 paper on the Clara Framework. This is by far the most concise introduction to Clara; therefore I hope that people will find it more accessible than my thesis. download the paper here
Abstract: Researchers have developed a number of runtime verification tools that generate runtime monitors in the form of AspectJ aspects. In this work, we present Clara, a novel framework to statically optimize such monitoring aspects with respect to a given program under test. Clara uses a sequence of increasingly precise static analyses to automatically convert a monitoring aspect into a residual runtime monitor. The residual monitor only watches events triggered by program locations that the analyses failed to prove safe at compile time. In two-thirds of the cases in our experiments, the static analysis succeeds on all locations, proving that the program fulfills the stated properties, and completely obviating the need for runtime monitoring. In the remaining cases, the residual runtime monitor is usually much more efficient than a full monitor, yet still captures all property violations at runtime.
C# implementation of Arithmetic Coder
Eric | August 13, 2010
Quite a while back, Malte Clasen, Joachim Kneis and I wrote a seminar paper on Arithmetic Coding. Apparently it’s not a bad paper, as it has been heavily cited. In particular, people appear to appreciate Malte’s C++ implementation of Arithmetic Coding, which fits on a couple of pages. This week, Sina Momken emailed me a very nice re-implementation of the coder in C#. The implementation is available in source from our AC website. Thanks Sina!
Lecture on Soot, Hands-on Tutorials on Clara
Eric | August 12, 2010
Dear all, for all of those of you who happened to be in Chile in November: I will be giving a lecture about the latest techniques in analyzing Java programs with Soot at the 3rd Summer School on Programming Languages, which is co-located with the Chilean Computing Week. You can find more information here. At the same even, I will moreover be giving a hands-on tutorial on Clara (“Partially evaluating finite-state runtime monitors ahead-of-time”), which is likely going to be similar to my RV tutorial.
TamiFlex 1.1 released
Eric | August 4, 2010
I am happy to announce that today we released version 1.1 of TamiFlex, our tool suite for dealing with reflection and custom class loaders in static analysis. Version 1.1 not only features several minor bug fixes but a completely new component called the Booster. Previous versions of TamiFlex required static analyses that were “TamiFlex-aware”, and at the current time the only such tool is Soot. The Booster makes TamiFlex compatible with virtually every static-analysis tool for Java bytecode: it transforms the original program into a new program version that is enriched with “materialized” versions of the originally reflective method calls, now in the form of standard Java method calls. Because these calls are now materialized in the code, static-analysis tools will discover them instead of unsoundly ignoring the calls.
ISSTA 2011
Eric | July 27, 2010
As publicity chair for ISSTA 2011, it is my pleasure to invite you all to Toronto, Ontario for July 17th-21st, 2011.
Toronto promises to be an exciting venue and our excellent program committee will certainly do its best to provide an great program. However, a conference is nothing without strong research papers! You are invited to submit technical papers describing original research in testing or analysis of computer software. Papers describing theoretical or empirical research, new techniques, or in-depth case studies of testing and analysis methods and tools are welcome.
You can download the full call for papers on the right. Workshop proposals are due Friday, November 19, 2011 and research papers on Friday, February 4, 2011.
Finally, if you wish to promote ISSTA yourself, you can download a web banner here.
3rd NASA Formal Methods Symposium
Eric | July 26, 2010
The NASA Formal Methods Symposium is a forum for theoreticians and practitioners from academia, government and industry, with the goals of identifying challenges and providing solutions to achieving assurance in mission- and safety-critical systems. The focus of the symposium is on formal methods, and aims to foster collaboration between NASA researchers and engineers and the wider aerospace and academic formal methods communities. The symposium will be comprised of a mixture of invited talks by leading researchers and practitioners, presentation of accepted papers, and panels.
Important Dates
Submission deadline: December 19, 2010
Notification of acceptance/rejection: January 21, 2011
Final version due: February 18, 2011
Conference: April 18-20, 2011
Reducing Configurations to Monitor in a Software Product Line
Eric | July 26, 2010Joint work with Chang Hwan Peter Kim, Don Batory, and Sarfraz Khurshid, to appear at RV 2010.
Abstract: A software product line is a family of programs where each program is defined by a unique combination of features. Product lines, like conventional programs, can be checked for safety properties through execution monitoring. However, because a product line induces a number of programs that is potentially exponential in the number of features, it would be very expensive to use existing monitoring techniques: one would have to apply those techniques to every single program. Doing so would also be wasteful because many programs can provably never violate the stated property. We introduce a monitoring technique dedicated to product lines that, given a safety property, statically determines the feature combinations that cannot possibly violate the property, thus reducing the number of programs to monitor. Experiments show that our technique is effective, particularly for safety properties that crosscut many optional features.
Download the paper here.
Tandem…
Eric | July 22, 2010
Tandem is not just a bike with two seats, it also means “at last” in Latin. At last I received my Ph.D. Diploma today! After only eight months of waiting time –yeah! (clap) Guess in what language it was written? Click the photo…
I hope I will be able to translate it at some point. For US immigration officers this appears to be too hard of a job. 🙂
Update: Here is the text and English translation. Thanks to Nicholas Greco!
