Applied Formal Methods

DANSAS 2011 trip summary

2011-08-24T10:41:00.001+01:00

Dermot Cochran and I attended DANSAS 2011 last week at SDU in Odense.

There was a healthy turnout of DK static analysis folks, particularly from Aarhus. I think that ITU was somewhat underrepresented though (hint hint).

The talks ranged in topic considerably and mainly provided a way for people to get to know what others were interested in lately, what new topics were popping up in the area, etc.

Zhendong Su from UC Davis gave an invited talk about dynamic and static program analysis for secure web applications. It was fairly pragmatic and straight-forward, but shows how focusing on a new problem with old techniques can really pay off.

Kevin Millikin, one of the authors of the V8 JavaScript compiler at Google (and an Aarhus PhD graduate from Olivier) gave the final talk about Crankshaft, their new compiler that does some static analysis of JavaScript. Again, this is all about doing great engineering and applying compiler and static analysis techniques that are 10-20 years old to modern problems and making a huge impact.

All in all I enjoyed this year's (and last year's) DANSAS and plan on going back to continue to make connections, see what people are up to, and help the community thrive.

Microsoft Research Software Summit trip report

2011-04-20T08:55:00.002+01:00

On Wednesday to Friday of last week I attended Microsoft Research's first European Software Summit in Paris. Basically Microsoft Research (MSR henceforth) invited about 150 high-profile researchers that they work with, want to work with, want to influence, etc. to come to Paris on their nickel and hob-nob for a few days.

The main themes were in areas in which Europe and MSR are both strong and doing novel stuff: multicore/parallelism, semantic computing, (empirical or rigorous) software engineering, web-scale data-driven research, cloud and services, verification, natural user interaction, tool-centric pedagogy, bug and malware detection, reconfigurable computing, and open source (!).

Keynotes came from Ken Wood, Tony Hey, and my friends Wolfram Schulte and Brendan Eich.

There were workshops on the role of funding agencies and industrial research in promoting CS education, SAT/SMT solvers, and sexy types, tutorials on Microsoft's .NET Gadgeteer and the future of F#, and panels on verification in the embedded application industry and speculations about software research in 20 years.

What did I learn?

MSR continues to do outstanding work and hire really great (and surprising) folks while Microsoft proper continues to tell tall tales about Open Source. An example of a new surprising person working at MSR: I met Peter Lee who is now the managing director of MSR Redmond (!) rather than returning to CMU after his stint at DARPA.
I'll be investigating a couple of new technologies from MSR for research and teaching. For research, I'll be looking into FORMULA, a unified framework for specifying DSLs and model transformations. I'll also be looking into the new plugin architecture for their Z3 solver that we have used for several years. For teaching, I'll be looking into augmenting my current use Code Contracts and PEX with FORMULA, Gadgeteer, VCC, and F#. I'll also definitely be contributing to RISE4FUN.
Microsoft has a new competitor to Google Scholar called Academic Search. It claims that MSR is the #1 place to do CS in the world over the past ten years.
Mario Campolargo (principle scientific officer for the EU commission DG INFSO) promises that the new EU Framework program will be simpler, more rationalized, more flexible, etc. I won't hold my breath though.
Alain Chesnais (President of the ACM) is a nice guy and says good-but-balanced things about the connection between a professional organization like the ACM and MSR and the funding agencies.
Brendan Eich showed me some new stuff going on inside of the Mozilla Foundation. They continue to hire PhDs to do interesting empirical software engineering and tool-centric formal methods applied to dynamic languages. He also name-dropped me in his keynote, which was a nice nod.
Tom Ball (MSR), Ganesh Gopalkrishnan (Utah), and others have developed a very nice course package for parallel programming call PPCP. Good stuff.
Andy Gordon (MSR) continues to blow me away. Their new F7 type checker (F# with refinement types) that was presented at POPL'11 is amazing.
Denmark was represented by myself, Kim Larsen, Olivier Danvy, and Anne Elisabeth Haxthausen, the latter of whom I had never met.
I met a bunch of other folks face-to-face for the first time that I have known online for some time (some over a decade!) including several of the aforementioned folks and Nikolaj Bjorner, Jean-Marc Jézéquel, Ben Livshits, Conor McBride, Erik Meijer, Manuel Serrano, and Don Syme. (Yes, events like these are about networking!)

Beta release of Votail

2010-02-25T14:28:00.001Z

The first beta release of Votail is now available. Votail is an implementation of Ireland's method of Proportional Representation by Single Transferable Vote (PRSTV). The functional requirements derived from Irish electoral law are specified using Business Object Notation (BON) and the Java Modeling Language (JML). Formal methods have been used to verify the correctness of the software.

Choosing a Supervisor, part 8

2010-02-24T07:54:00.000Z

What kind of collaborator is your potential supervisor? Are most of their research papers written with their PhD students, with colleagues within their own university, with researchers elsewhere, or by themselves? Is their name the last name listed on every paper that comes out of their research group, or are they first authors on several? The answer to these questions gives you indirect evidence as to which type of collaborator they are.

Personally, I try to find a nice balance between these different strategies, avoiding the "my name goes on every paper because it is my research grant" approach that some supervisors demand. Some papers from my group are solely authored by yours truly (e.g., "Formally Counting Electronic Votes (But Still Only Trusting Paper)""); others are co-written by nearly every member of my research group because everyone pitched in and helped, each finding a facet that fit their strengths and interests (" CLOPS: A DSL for Command Line Options").

But not all supervisors work this way. In all honesty, some supervisors, due to over-commitment or neglect, only meet with their students once a quarter, even when their students are begging for supervision. Some you have to book a month in advance for a half and hour, and even then you are not guaranteed that they show up.

Others have an open door policy and, even though they have very full agendas, make time for their students whenever they are needed. I try to be this latter kind of supervisor, but on rare occasion I feel like the former.

The kind of supervisor that is always "missing" is actually a good supervisor for some kinds of PhD students. Hard-working, independent students who like to drill down on a topic for weeks or months in between taking breaths of air with nudges from their supervisor work well in such groups. But if you are the hand-holding type that wants lots of face-to-face time with your supervisor, or you do not really know what you love to do and are good at in research, I would suggest you stay away.

Choosing a Supervisor, part 7

2010-02-23T08:07:00.001Z

11. Attitude toward IP and Technology Transfer

Some researchers focus entirely on "pure" research, where one follows the research to its very end, damn the consequences or application. Others enjoy "applied" research, where the use and utility of the research is under direct consideration, and often guides, and sometimes even terminates, the work. These agenda extremes are extremely valuable, and we perform both in my research group.

But for research to see the light of day---for it to be in the hands of governments, companies or, dare I say it, the "public," research needs a evangelist, a support network, and a trusted base of experts. This is where those dreaded words, to some, like "spin-offs," "licensing," "copyright," "trademark," "patent," "lawyer," "venture capitalist," and more come to the fore.

What is your, and your potential supervisor's attitude toward Intellectual Property (IP), both with regards to the law and the state of practice, and what are your attitudes toward Technology Transfer (i.e., moving research from a lab to a real company)? Should research be publicly funded, open, and available to all immediately, whatever its use, utility, value, or impact? Should research be co-financed by public or private corporations, with explicit commercialization aims? Something in-between?

Does your supervisor know the state of software patents in the EU? Process patents in the USA? How and when to conduct a patent search? How to write, a better yet, obtain patent from the USPTO? Do they know how copyright law impacts scientific writing? Programming? Do they know when to choose a GPL, a BSD, or an X11-style license, and why?

Does your supervisor sit on any corporate boards? Are they a founder of a startup? Is that company still running? Did it raise a significant amount of capital? Attract a following? Make an impact? Are you interested in someday commercializing research?

Does any of this matter to you at all? If not, why not?

Choosing a Supervisor, part 6

2010-02-22T08:27:00.000Z

10. Gender Balance and Attitudes

What kind of attitude does your potential supervisor have to gender balance and women in computing? Besides the obvious gender equality statements one can expect, are they actively supporting or promoting women in computing?

In many branches of computing and engineering, and in North American and most of central to northern Europe, the ratio of women to men in computing is quite low. Happily, some researchers work in areas that, for a variety of reasons, are more attractive to women researchers and students than others. Others have a more difficult situation: for example, the number of active, visible women researcher in my sub-discipline worldwide is on the order of a couple of dozen.

How can this situation be addressed? Should this situation be worrisome? Do we need more women in computing, and if so, how do we achieve this goal? Attitudes about and answers for these questions classify supervisors as managers in sometimes surprising ways.

Personally, I come from research groups that had decent, but not fantastic, female representation. The groups I worked with at UMass and Caltech had perhaps 1 in 5 ratio. But ever since then I have had less success. This frustrates me.

For the past five years I have actively tried to recruit woman PhD students and postdocs. But of the perhaps 300 "cold" applications I have received and reviewed for hiring, I have only seen about 5 women applicants. I have also pursued hiring a handful of woman researchers, but none of these cases were successful.

I also give special invited lectures to woman undergraduate students and have participated in summer internship programs that focus on under-represented groups in computing (e.g., women, African-Americans, Hispanics, etc.). But all of these activities seem to have come to naught, at least in a direct and immediate fashion into my research group.

Obviously, if you are an outstanding potential PhD student or postdoc and wish to work with me, please get in touch!

Choosing a Supervisor, part 5

2010-02-19T09:29:00.003Z

Aside: Over the past few weeks I have been in the middle of a vacation in the USA, a move of my family to Denmark, and starting a new job at ITU. Apologies for the silence in posting.

9. Young vs. Old

Your potential supervisor typically must have a PhD, so this means that they are an "experienced" researcher, but how old are they? On the young side, typically a supervisor is of at least 25/28 years (EU/USA) in age. On the older side, since retirement ages vary from country to country, your potential supervisor might be nearing or into their 70s, or even their 80s. While it is inappropriate to discriminate based upon age, your potential supervisor's age does have repercussions.

Is your potential supervisor nearing retirement? Are they the super-star having just earned their PhD themselves? Something in between?

Supervisors that are at either end of the age spectrum present potential problems, none of which are insurmountable nor intimidating, but should be reflected upon.

A very young supervisor might have little-to-no experience with supervising research themselves. Some universities and supervisors insist that their PhD students gain some experience with supervision, either of undergraduates or MSc students, but this is by no means the norm. Likewise, many quality new professors in the USA obtained their positions directly out of graduate school, so they never held a postdoc position wherein they might have co-supervised a PhD student, a situation that is much more common in the EU.

Also, while one might communicate with a young supervisor more naturally, since you may be in (nearly) the same age group/generation, some people have difficulty working for and respecting a boss that is nearly the same age (or younger!) than themselves. This can be particularly problematic for returning students---can you work for a professor that is a decade your junior?

The dual of this situation is working with a supervisor that is several generations your elder. While they may have enormous amounts of experience and have graduated dozens of PhD students, their core attitudes and perceptions may reflect a different age. This can especially become a tricky situation in fast-moving fields like computing, where research that is five years old is sometimes considered ancient.

Also, to be blunt, an older supervisor may choose to retire, or may have health problems that lead to troublesome situations late in your career. What happens if you are in the final stretch of your PhD and your supervisor decided to retire and move to Florida or, in the worst case, passes away? What is your contingency plan for such a situation?

Choosing a Supervisor, part 4

2010-01-30T20:39:00.002Z

6. Talk to Ex-students

Perhaps one of the most important things you can do is to speak with current and ex-students of your potential supervisor. They will give you the real story of what it is like to work with him or her, what the research group's character is like, etc.

Some questions to ask include the following: How long does the typical student take to finish their PhD in your potential supervisor's group? What are the outliers like and why? Does the student feel like a peer of his or her supervisor, or are they more deferential? What fraction of students that start a PhD with your potential supervisor actually finish? Has the supervisor lost students to other groups or supervisors? How does the supervisor work with students? How much time does the supervisor give to their students? Do they have an open-door policy?

I am certain that the more outgoing senior graduate students in the group will be happy to share their experiences. If none are willing to speak up, consider that a sign in and of itself. Recent graduates are also much more likely to give you the inside skinny, for obvious reasons.

7. Public Presence

Being a successful scientist is half about doing the science and half about communicating the science. Some scientists communicate strictly through the peer-reviewed research paper, while others use every new "Web 2.0" medium that pops up in recent years?

How up-to-date is the potential supervisor's web presence? Do they use Twitter? Have a blog? Use Facebook? Do they convey research results in a modern and timely manner, or are they more "old fashioned?" Does any of their research occasionally hit printed mainstream media? Are there press releases? Is your potential supervisor ever quoted in the media or seen on television?

What is your attitude toward communicating results? What is the role of the citizen scientist and her relation to the media?

8. Attitude toward Teaching

What is your potential supervisor's attitude toward teaching undergraduates and graduate students? Do they volunteer to give guest lectures at high schools, summer interns, incoming students, and other non-core student cohorts? Do they connect teaching with their research, or are these two main facets of their work lives disconnected?

Or do they think of teaching as an unwelcome burden, their time being better spent focusing entirely on supervising or conducting research?

What is your attitude toward teaching? Do you want to learn from and be inspired by a great instructor, or is teaching a necessary evil? Do you want to work with someone who spends time writing textbooks, or is the only thing worth writing the paper in the number one conference in the area?

Choosing a Supervisor, part 3

2010-01-27T15:40:00.005Z

This is part three of the post, Choosing a Supervisor.

The next few questions I suggest asking yourself before choosing a supervisor are as follows:

3. What is their noteriety?

The personality and demeanor of a supervisor are critical to your suceess. In particular, their personality needs to "fit" with yours.

Some people work very well under high pressure with a very critical supervisor; others crumble. Some want a very hands-off supervisor and lots of independence. Others want a kid-glove and only to hear positive feedback.

Each supervisor has a very different approach to interacting with PhD students, and often that approach is very consistent over a multi-year timeframe. Some supervisors are just asses, plain and simple, but because they are research superstars, it is tolerated.

Do you want to work for an ass? A nice guy? An introvert? An extrovert?

4. How do they work?

Different researchers work different ways. To be a successful world-class researcher requires discipline and commitment, but it does not necessarily require giving up a social life, a family, and television. The way that your potential supervisor works oftens tells you how they expect you to work as well.

Are they an 9 to 5 type, or will you find them in their office at 11pm? Do they work directly with students in their lab, or do they only "manage" research? Do they seem to work very hard, but without a lot of results, or vice versa? Do they expect their students to work as hard and long as they do, or much harder or longer? Do they have families? Kids?

Do you want to work for a workaholic with a family that they never see? Or perhaps a professor that has found a good balance between family and work? Or a single person completely committed to their career?

5. Theoretician vs. Experimentalist/Breadth vs. Depth

Like many fields of science, computing sees some research that is purely theoretical and often requires nothing more than a pencil, a paper, and grey matter. Other groups eschew such research and focus entirely on an experimental approach, building realistic, non-trivial systems that are evaluated through quantitatively analysis.

The notion of "experiment" also varies from sub-discipline to sub-discipline. Within some communities the notion is quite ad hoc, while in others it is very rigorous.

Finally, some research groups are very focused and deep, exploring one specific topic for many years. Others are quite broad, permitting their students to choose topics from a broad set of topics---sometimes all of computing!

What kind of group do you want to be a part of? Do you prefer rigorous mathematical foundations, or would you rather just build and measure systems? Perhaps you see the value and attraction of both approaches? Do you want to be the single world-expert in one highly-focused topic, or would you rather play in a bigger sandbox, perhaps not digging as deeply?

Applied Formal Methods at National Taiwan University

2010-01-20T23:06:00.006Z

On 1 January, Joe wrote about his New Year's resolutions, one of which involved doing more "public" writing in 2010. He said that he had tried to draft me into this resolution with him, but was not sure whether he succeeded. He did, in fact, succeed... and so my goal, like his, is to write or edit at least 1,000 public words per day (on average).

Unfortunately, I've fallen somewhat behind. Today is 20 January, and so far this year I've submitted an 9 1/2 page paper to QSIC 2010 and given a public talk (more on that later) for which the slides (available here) comprise about 1,500 words. I figure that puts me at about 10,000 words... and therefore behind by about 10,000 words (after this post, I'll still be behind by about 9,000 words).

One of the reasons I've fallen behind (and this is not meant to be an excuse) is my holiday travel - from 31 December to 13 January, I was in Tokyo and Taipei; both are very interesting places to visit, and Tokyo at the New Year is especially interesting because that's pretty much the most important holiday on the Japanese calendar (unlike much of the rest of East Asia, where the New Year on the Chinese calendar is the most important holiday). Thus, there are multiple special events: New Year's Eve celebrations, the Emperor's annual address to the people and the opening of the Imperial Palace grounds on 2 January, special food, and of course fukubukuro (lucky bags). Sadly, I missed my chance for a lucky bag at the Apple Store in Ginza by several hours... but I digress.

The reason for mentioning my holiday travel here at all is the public talk I gave at the Department of Computer Science and Information Engineering at National Taiwan University, entitled "Building Reliable Software with Applied Formal Methods: A Brief Overview". The talk was arranged when I told a contact of mine there that I was going to be in town, and fellow Caltech Ph.D. Hsuan-Tien Lin was my very gracious host. He told me that nobody in the department really had any experience with applied formal methods, so I prepared the talk as an overview of the tools and technologies we use in our verification-centric software engineering process (described in A Verification-centric Software Development Process for Java).

I initially expected that the talk would be received in much the same way as the (very similar) talk I gave at KITECH last August, where there was also little in the way of formal methods experience in the audience; at KITECH the response was one of polite interest and some good questions were asked, but there was an overall sense that they were not likely to adopt any of the techniques I described. Imagine my surprise, then, when I ended up eating lunch with (and later answering questions from) Yih-Kuen Tsay, a professor in NTU's Department of Information Management, who was not only familiar with JML and BON but also knew specifically about KindSoftware and the Mobius PVE! Dr. Tsay is, by a remarkable coincidence, an academic nephew of mine and Joe's; his Ph.D. advisor, Rajive Bagrodia, was one of Mani Chandy's students at UT Austin.

Dr. Tsay teaches courses entitled "Software Development Methods", "Software Specification and Verification", and "Automatic Verification" (among others). He told me that he had considered using JML and its related tools (including Mobius) for his courses but that, for several reasons (primarily having to do with the maturity of the tool support), he is currently using UML/OCL and Frama-C instead. We had a very interesting discussion where he told me that he would very much like to be able to use JML in his teaching, and I told him a bit about OpenJML and the current Mobius PVE release. He also stated that, for better or worse, UML and OCL are industry standards, and wondered if we (the JML community) had ever given any thought to attempting to standardize JML, or some subset of JML, through an international standards body.

I actually don't know whether the JML community has considered attempting a "JML Standard" or not, though I suspect not... and I also don't know whether it's a good idea, though again I suspect not. My instinct is that the standardization rabbit hole is one that we (as academics) would be better off not diving into, lest we never emerge to do non-standardization work; but at the same time, actually having a standard might encourage industrial tool support, which would facilitate said non-standardization work. Certainly, it's interesting to think about what the ramifications might be.

As for the talk itself, it went quite well. It was on 8 January, the last day of instruction for the autumn semester; they have 18-week semesters at NTU, which makes me incredibly jealous, as I always have to struggle to fit material into my 10-week quarters here at UWT. The students and faculty that attended seemed quite interested, and I have no doubt that if there were easy-to-use, modern tool support for the development method I described, many of them would try it and some would end up adopting it. If only there was a way to entice more people to contribute to OpenJML development...

Choosing a Supervisor, part 2

2010-01-19T02:45:00.002Z

This is part two of the post, Choosing a Supervisor.

The second question I suggest you ask yourself with regards to choosing a supervisor is:

2. What is their impact and its timeliness?

Some researchers make their reputation once, so to speak, often early in their careers, then sort of just glide on it their whole lives.

Others reinvent themselves every 5-10 years, either by moving to new fields, writing high-impact books, making new fantastic discoveries or inventing useful new concepts. Perhaps they also co-create a startup and give technology transfer a try.

Do you mind working for someone who "was good back in the 80s" when it is 2010?

Choosing a Supervisor, part 1

2010-01-17T21:31:00.003Z

I have heard the metaphor that choosing a supervisor for your PhD is like choosing a spouse or a parent.

I think that, while both of these have a ring of truth to them, the better metaphor is that your supervisor is like choosing who you, the future you, in a decade or two's time.

When I first went to graduate school at the University of Massachusetts, Amherst, I was admitted as one of thirty-odd incoming miscellaneous postgraduate students, as is typical for the vast majority of large PhD-grading research-centric PhD programs in the U.S.A. The majority of time during our first two years was taking graduate courses in computing, being a Teaching Assistant (TA) and helping teach undergraduate (and sometimes graduate) courses, and preparing for our PhD exams and/or building our portfolios.

I was offered, and declined, a RA position by the LASER group, led by Profs. Lori Clarke, Lee Osterweil, and Jack Wileden. Other students in the group at the time included my distinguished colleagues Peri Tarr, Matt Dwyer, and Alex Wolf was a semi-recent graduate.

Their group, at least at the time, ran using the "cog-in-wheel" approach to research groups. In that approach, one of several about which I will write in a future post, students are "given" a project on which to work, and typically that project becomes a key component of their PhD. I was interested in finding my own topic, and at the time I was consumed with distributed systems and computer graphics, so I felt the LASER group was not a good match for me. In the end, after teaching for a year, I took a part-time job as a system administrator for the department and ended up doing an MSc with Chip Weems.

Had someone given me advice like that which I am writing now, I likely would have stayed in that group and gone on to have an equally good career, perhaps with fewer fits-and-starts (good) and less variety (bad).

Now, several universities, companies, degrees (and fifteen years) later, I have seen the full gamut of PhD supervisors, good and bad, and witnessed the inspiration and chaos they instill in research students, fresh and hoary.

Consequently, here are the questions that I think you should ask while choosing a supervisor. I'll post one a day for a week or two, then summarize in a final post.

1. What is his/her research reputation?

Do you want to work for a superstar or an everyman? If you do not really care about their research impact, then there isn't anything to investigate.

But, if you are interested in someone who is very good (i.e., with an international reputation, well-respected, makes an impact, etc.), look to see what program committees they are on. You want to see all "A" profile conferences and better. Look also if they are on the organizing committees of any long-lived high-profile, high-quality conferences. Also look to see if they are frequently invited to give kenotes at major conferences.

Do you want to work for a supervisor who has never been on a program committee, or has only been on committees of faceless conferences of dubious reputation?

Soundationalists

2010-01-04T14:35:00.000Z

Soundness is a much-maligned metatheoretical property.

To the theoretician, soundness is an obvious given: if your theory is not formally sound, it is useless. To remind the reader, a logical theory is sound if and only if its inference rules prove only formulas that are valid with respect to its semantics. In most cases, this means that its rules have to preserve some notion of "truth," so that in each step of a proof, validity is preserved. Even wikipedia says, "Soundness is the most fundamental property in mathematical logic."

To the practitioner though, soundness is a desirable, but not necessarily mandatory, property enjoyed by few tools. Most tools that are "sound" end up being too difficult to use, as they have too many seemingly arbitrary restrictions due to assumptions made in defining the underlying theory (e.g., Spec#), or they require interactive use by experts (e.g., the LOOP tool).

In counterpoint to these "sound" tools (more on the use of those double quotes later), automated tools that require little intellectual or fiscal investment are the only tools that are broadly adopted and make an impact in recent years. But automation comes at a price, and for complex systems analysis, that price is usually soundness.

Unfortunately, this second perspective is lost on many theoreticians. They not only insist that soundness is a mandatory property for a logical theory—the quality research of mathematicians who develop deviant (non-classical) logics and paraconsistent logic systems notwithstanding— they also demand that all tools be sound and that any tool that is not sound is worthless. I call these kinds of researchers "soundationalists".

I have several problems with the soundationalist point of view.

Firstly, the soundationalist is forcing a value judgement on others. Inconsistent systems are all around us, and yet we, as humans, work with and within them everyday, with aplomb. Formal mathematical systems, whether they are logics or tools build upon logical foundations, are no different. The humans that work with such systems will adapt to their particular quirks, whether the quirks are harmless idiosyncrasies of operator precedence or more serious challenges, like the fact that a particular theory has dangerous corners that are not know to be sound. Remind the soundationalist of the consistency issue with set theory that they will quickly change the subject.

Secondly, I find that very few soundationalists have practical experience in building or using tools grounded in formal theoretical foundations. They are often the researchers who claim that translating a theory into practice is "just a matter of engineering." Thus, my problem is that the soundationalist has lost their connection with the "reality" of our discipline.

Alternatively, they are the ones that delegate the dirty job of realization (i.e., implementation) to their graduate students, never involving themselves in issues of architecture or programming, and then proclaim that their software is sound because their theory is sound.

Whenever I heard this claim I immediately presume the speaker does not know what they are talking about or they are trying to mislead me. The myriad of design and implementation choices, trade-offs, and challenges that accompany implementing any formally grounded software system leave dozens, if not hundreds, of soundness compromises to creep in. In my entire career I have yet to see the implementation of a sound formal system result in a sound formal tool with an accompanying mechanical proof of soundness of both claims.

Lastly, the soundationalist is ignoring reality. Non-trivial tools grounded in formal systems must make compromises if they are to be automated, since very few interesting and useful problems are decidable in the first place. A verification system that attempts to handle simple arithmetic is already over the precipice; one that claims to reason soundly about procedural or object-oriented programs—programs that are the concrete realizations of some of the most complex mathematics ever invented by man—is simply being specious.

I propose an alternative strategy to dealing with soundness.

First, by all means attempt to develop sound logical theories, but do not shirk your responsibility in proving your theory sound. A hand-waving proof in a short paper is persuading only to the persuaded. Mechanically formalize your theory in an appropriate logical framework and show how smart you are by closing the book on soundness by developing a watertight soundness proof in all its gory and glorious detail.

Secondly, learn a little bit about alternative, possibly unsound, strategies in developing and using non-traditional logics and logical frameworks. There are so many interesting pieces of work out there with broad application, ranging from Haack's survey of deviant logics [1] to paraconsistent logics' use in knowledge representation, abductive reasoning, and belief logics [2-6].

We need to see more mechanized work in these logic. I would love to use or develop a non-classical model checker. The application of paraconsistent reasoning to the hard problems plaguing (or, more commonly, ignored by) those working in the "semantic web" and "agents" research areas represents some interesting, novel, and non-trivial low-hanging fruit for the right research team.

Lastly, if you build a tool based upon a sound theory, (a) document every design and development decision you make that possibly compromises soundness and (b) make it a mandatory feature that your tool has a metatheoretical warning system, much like ESC/Java2 does [7]. Your users will be better informed about the reasoning that they are actually performing and they will better understand the concessions that they must make to use your tool for its intended purpose.

Also, of course, you will be more honest about your scientific product, and everyone likes a self-deprecating scientist that spends serious intellectual effort pointing out their own flaws and their competitors successes.

[1] Susan Haack, Deviant Logic. Cambridge University Press, 1974.

[2] G. Priest and R. Routley and J. Norman, Paraconsistent Logic: Essays on Inconsistent. Philosophia, 1989.

[3] Max Urchs, Essays on Non-Classical Logic, chapter "Recent Trends in Paraconsistent Logic." World Science Publishing, 1999.

[4] Diderik Batens, Frontiers of Paraconsistent Logic. Taylor and Francis, Inc., 2000.

[5] Diderik Batens, Paraconsistent Logic: Essays on the Inconsistent, chapter "Dynamic Dialectical Logics." Philosophia, 1989.

[6] C. Damasio and L. Pereira, Handbook of Defeasible Reasoning and Uncertainty Management Systems, chapter "A Survey of Paraconsistent Semantics for Logic Programs." Kluwer, 1998.

[7] Joseph Kiniry, Alan Morkan, and Barry Denby. "Soundness and Completeness Warnings in ESC/Java2". The 5th International Workshop on the Specification and Verification of Component-based Software (SAVCBS 2006). Portland, Oregon. November, 2006.

Unshipped Software Does Not Exist

2010-01-03T12:13:00.002Z

In much of computer science, at least the "systems" variety, an enormous amount of effort is spent designing, developing, and experimenting with software systems. Meaning, we write programs to make concrete our new ideas, show off our inventions, and validate our claims.

In the world of hard science, this engineering, albeit of the software kind, is more akin to experimental science than theoretical. We are like the physicists who build super-colliders, smash together atoms, and measure the results to validate or invalidate hypotheses posed by ourselves or others.

Despite what the theoretician might tell you, developing a complex software system is non-trivial and is more than "just a matter of engineering." It is often an incredibly complicated endeavor that continuously opens up (and sometimes closes) new research doors, most of which we never publish. In my experience, merely shipping a complex software system takes about the same amount of time as writing a conference paper.

And thus we have our dilemma: we have an experimental science, that of systems-based computer science, whose sole output, for the vast majority of researchers is exclusively the twelve page conference paper, in which only the Smallest Publishable Unit (SPU) of the work is described.

Nowhere is the full software system described so that others can replicate the "experiment." Though we are a discipline that thrives on abstraction, you essentially never see a full, or even partial, specification of a research software system.

And obtaining a copy of the concrete system designed and built by researchers over many man-months? Forget it. It is always "not quite done" or "needs to be cleaned up." Or perhaps it is "pending an IP review" by a technology transfer office. Heck, some researchers simply do not answer their emails or return phone calls when I ask them for a copy of their system!

More often, the reason scientists do not ship is more pragmatic and more cynical. Shipping software is simply not directly rewarded in nearly all Universities. Tenure reviews and promotion panels sometimes even state that developing and shipping software is a waste of time, time better spent on writing peer-reviewed papers.

In my view, this situation is untenable and this behavior is unforgivable. This is not legitimate science or engineering.

If you do not ship a research software system, it does not exist.

Like the physical sciences, where one cannot publish a paper unless an experiment is described in excruciating detail and data is often made publicly available, I believe that one should not be permitted to publish results based upon an unshipped and undescribed system.

When I review research papers that discuss results coupled to software systems, the first thing I search for in the PDF is "http." If I cannot find a mention of how and where to download the system in question, my warning bells go off. If a Google search turns up nada, I reject the paper, as simple as that. Hollow promises of shipping after publication or at some later date are ignored, as they are so often unfulfilled.

I also know from personal experience how rewarding developing and shipping a software system can be.

You are opening your heart and head to the world by showing everyone exactly what you are made of. Sure, you may have fewer papers than some competitors, but your limited time budget for writing means that you must more tightly prioritize writing goals and publication targets.

The notion of SPU goes out the window as you want to put as much into each research paper as you can fit, rather than as little as will be accepted for publication.

Finally, if you develop systems that are useful and usable, you gain an audience of industry and academic users that is typically at least as large as the number of people that would have read that conference paper or two you did not write, and typically orders of magnitude larger.

My advice to the young PhD Computer Science student? Ship your software; you won't regret it.

RSpec

2010-01-02T10:08:00.004Z

I enjoy discovering when old, good ideas from the research community eventually trickle their way out into common practice, but sometimes what you discover surprises you.

For example, contracts are a great idea that should see wider use, especially in languages that provided assertions from day one. But after you discover the nth framework/tool for providing contracts in a language like C++ or Python that does not support inheritance or visibility, one gets a little deflated.

This week I accidentally came across RSpec from the Ruby community. It caught my eye initially because it is described as a "behavior-driven development tool" and one of its popular tutorials states on line one: "Behavior Driven Development is specifying how your application should work, rather than verifying that it works.", this sounds like a framework for me. Moreover, since contracts are at the core of behavioral interface specification languages (BISLs) like the Java Modeling Language (JML), and I'm "one of the JML guys," then I should get excited about RSpec, or at least learn something from it. But before I dig into RSpec, let's reflect upon Ruby a bit.

I learned Ruby when it had just "leaked" out of Japan many years ago. The only English documentation on the language then was a fragment of the API docs, and thus I had to learn the language by reading other peoples' code. I like Ruby. It purposefully or accidentally intelligently synthesizes some of the best ideas of Smalltalk and object-based languages with a prototype-based feel. By prototype-based feel I mean languages like JavaScript, Tcl and, I'm told, used in several of the scripting languages that I mentioned yesterday, namely Io, Logtalk, Lua, Omega, and REBOL. My experiences with these kinds of languages derives from the literature, namely Abadi and Cardelli's "Theory of Objects" and papers about the Self language. The fact that it gives you some access to its metaclass system, a la Smalltalk, in a relatively clean API unlike, say, the horrid APIs of Python and Perl, is also compelling.

Consequently, I have written a few thousand lines of Ruby, including some of the server-side processing for my research group's website, and thought it would be nice to see a clean OO scripting language like Ruby catch on (as it has, in spades).

So, I hear you say: "Hey, a simple OO language with a clean metaobject framework is ripe for the application or dependable software engineering principles, Joe!" I would say you were right, so lets see what has happened in the World of Ruby... so, back to RSpec.

The first thing to note is, while the 'B' in "BDD" means "behavior," it is not literally in the sense of BISLs, but instead is the "behavior" of the "Agile" community. *sigh* This already starts to worry me, but lets not throw the baby out with the bathwater, because sometimes riding on the coattails of a populist movement like "agile programming" (or "aspects" or "Java," for that matter!) is just a smart mechanism to effect change.

The API and common use of RSpec guides a developer down the path of connecting informal English sentences using modal verbs like "must" and "should" and code fragments which interpret the informal specification. Thus, "behavior" in this context is the informal, manual specification and linking of traditional requirements and hand-written unit tests.

Now, anyone familiar with my work in BON and verification-centric development will know that I think codifying requirements, domain analysis, and features in structured English is a Good Thing. And we have been developing a formal refinement between informal specifications in English and formal artifacts like requirements, concepts, tests, types, and assertions (look for a paper on this in 2010). So the juxtaposition of English and code is unsurprising to me.

The codification of assertions in the API is also interesting. Having methods like "should" and "should_not" are akin to jUnit methods like "assertTrue" and "assertFalse," though fit better with the vernacular of the domain. Permitting the definition of pre and postconditions of unit tests via "before" and "after" methods, akin to aspects and straight from the world of CLOS and MOP, is also nice to see. There is also integrated support for mock objects and the use of lambda expressions to talks about state in the pre-state of a method call is cute as well.

So in the end, I think RSpec is a pretty nice framework for specifying the behavior of Ruby code, but only if you are willing to accept the fundamental testing premise of agile programming: that hand-written unit tests should specify the behavior of a system. My criticisms of this approach are not unfamiliar. Hand-written executable tests are only maintainable at high-cost and are expensive to write early if one does not have (1) a fairly solid understanding of a domain and (2) pleasant customers who do not change requirements all of the time.

In other words, I am still unconvinced that in the key areas where agile programming is supposed to shine their fundamental tenant, that of test-driven development, holds true. If you are an agile practitioner and have evidence of this claim, please speak up!

I will write more on RSpec later this year after I get a chance to really take it for a test drive.

New Year's Resolutions

2010-01-01T12:42:00.002Z

One of my New Year's resolutions is to do more "public" writing in 2010.

As it is, I do a lot of "private" writing in the form of coursework, exams, slides, reports for grants, grant writing, thousands of emails, consulting, etc., and only a moderate amount of "public" writing like public reports, peer-reviewed papers, software manuals, web pages, and an occasional blog post. I have tried (and succeeded in?) drafting my friend and colleague Dan Zimmerman into this task, proposing that we each write or edit at least 1,000 public words per day. Every day I do not reach this goal I have promised to donate 1,000 cents (i.e., $10) to the GOP. As you can imagine, this punishment is very motivating.

Up until about 2007, I used to learn a new programming language every few months. Consequently, I now know something between 40 and 50 languages. I want to reboot that effort, as 2008 and 2009 were exciting years for new programming languages. (In recent years my attention has been more focused on revision control systems, higher-order and first-order theorem provers, and new logics.)

To "know" a language means that I: (1) can read it immediately, (2) have written at least several lines of non-trivial code in the language and, (3) after a few hours refreshing myself, if I have not written a program in a language for several years, I can write arbitrary programs in the language.

The high-profile languages that are at the top of my queue are Clojure, Go, Haskell, and Scala. I can read all four, but have never written programs in any of them. I also know quite a bit of the theory behind each language, and have reviewed research papers using them, but I need to bury myself in them for a few weeks to really get my money's-worth.

Performing a search on "programming," "language," and "compiler" in MacPorts also reveals a whole bevy of languages and compilers that I do not "know": arc, argh!, aspectj, bc, boo, clojure, cyclone, gdc/d-mode, embryo, erlang, ferite, ficl, fsharp, gforth, gnudatalanguage, gri, groovy, guile, ici, icon, Io, jekyll, logtalk, lua, mawk, mercury, mozart, ncarg, nesc, nice, nu, Omega, oorexx, pike, pure, q, qore, R, rb-kwartz, rexx, scala, shakespeare, slang, snobol4, squirrel, strategoxt, xotcl, yabasic, 4th, bf2c, cm3, distcc, gpc34, gprolog, gwydion-dylan, ikiwiki, inform, mono-basic, newt0, nhc98, nqc, objc, pnet, ragel, swi-prolog, tom, vala, yap.

I have a special interest in the scientific programming languages like gri, ncarg, and R due to a grant proposal I am working on, so they will get earlier attention. Historic languages like Dylan, Erlang, Forth, Icon, and SNOBOL are also eye-catching. Languages that seem to often come up in online discussion like Cyclone, D, F#, Guile, Lua, and Pike are are prioritized. Finally, I use some of these systems regularly, like bc, but not to their full extent. If I can get

through half a dozen of these this year, I will be happy.

What will I do with these new languages? On thing I am debating is writing a minimal extended static checker using FreeBoogie for each in the language itself. Of course, there are many other projects constantly happening in my research group, so there are undoubtedly implementation opportunities there too.

I will report on my progress on these efforts in this blog. I will also be using this blog to reflect upon new theories, tools, and technologies that I come across this year.

After all, why not take a big move to a whole new university as an opportunity to reinvent oneself via self-reflection?

Current Trends in Computer Science (Conference)

2009-06-12T19:40:00.008+01:00

I participated in a two-day conference organized by the Institute of Theoretical Computer Science in Prague entitled "Current Trends of Theoretical Computer Science" (STTI 2009). The presentations were invitation-only, which was mainly based on the criterion that the invitee had a publication at a well-established conference. The presentations were carried out in Czech and Slovak, which was a common source of amusement as few were used to that.

Talks

The number of talks was rather large so let me mention some representatives. The main talk was given by Viliam Geffert on finite state automate minimization. Minimization of standard DFAs is a well-known problem, this talk has addressed minimization modulo introducing finitely-many errors in the output of the result of the minimization. The motivation for such types of reduction is that if a certain device is running for an unbounded period of time, a finite number of errors at the beginning does not pose a problem.

Matus Mihalak presented a nice algorithmic problem in which a number of cops are guarding a certain region of a graph against a robber. Some complexity results were presented. For instance that the problem is NP-complete when the graph is a tree.

Another nice algorithmic problem was solved by Pavel Surynek: how to move a group of robots to desired destinations in a graph; with the additional objective to find minimal plans. This problem is motivated by traffic or warehouse organization. Pavel has targeted a special case when the graph is 2-connected. For intuition, Lloyd's 15 puzzle is a special case of this problem.

A problem from the bio-informatics was presented by Brona Brejová. Given a Hidden Markov Model (HMM) and a chain of transitions, one is to find the most probable sequence of states in the model that would correspond to the sequence of transitions. The classical algorithm solving the problem uses memory proportional to the length of the transition-sequence and number of states in the HMM. This is too much for the examples coming up in bio-informatics and thus Brona and her coauthors devised an online algorithm discarding unneeded memory.

Several talks were on complexity classifications. Stanislav Živný presented some of his results on so-called submodular polynomials. These are pseudo-boolean polynomials satisfying an additional constraint called submodularity. Minimization of these polynomials can be done in cubic time for quadratic polynomials. Stanislav has been investigating for which polynomials can minimization be translated into minimization of quadratic ones.

Jiri Srba gave an overview of recent complexity results for Visibly pushdown automata. Those are such pushdown automata where each operation must always push/pop a fixed number of symbols from the stack. These automata are interesting for program verification as equivalence is decidable (in program analysis the stack models the callstack). One of the mentioned results of Jiri was that deciding bisimulation for visibly pushdown automata is EXPTIME-complete.

Eva Jelínková has presented a problem from the graph realm. Eva has investigated the complexity of deciding whether a clustered graph can be drawn nicely in a plane. A clustered graph is graph in which nodes may be contained in clusters; clusters are either disjoint or one is a subset of another. By nicely I mean that the clusters can be drawn as closed curves that do not intersect.

Rastislav Královic presented a problem from the networking domain. Rastislav has investigated how strong of an opponent can we have when the game is that we need to send a message in a network and the opponent is allowed to discard certain number of messages. One of the presented results was that a message can still be delivered even if the opponent can discard all but one message in each step.

Problem Section

An interesting part of the conference was the Problem Section, where whoever wanted presented a small (open) problem. I have presented a problem that I've bumped into recently and Radu wrote up here (I was a bit surprised that I haven't got an answer or pointer (yet)).

Martin Klazar has presented a so-called Skolem's problem which was is it decidable that a recurrent sequence hits a 0?

Libor Barto has presented a hard-core question, what is the minimal tree for which H-coloring is NP-complete?

Summary

All in all, I would like to say that it was a nice experience. All participants came neither for fame nor for money and still the talks were given in an excellent quality. I'm glad that I went as I enjoyed the overall spirit of the conference and not only I learned about the result of my countrymen but about theoretical computer science in general.

P.S. apologies to those whose names are not spelled properly but my patience is quite limited when it comes to diacritical problems :)

P.P.S. Mr. Nesetril, the program chair, told me that it is not correct that anybody could have participated in the Problem Section as he filtered the topics beforehand.

Program verifiers are complex

2008-12-15T13:00:00.000Z

I've recently found out that epitome is not only a Romanian word but also an English one. The discovery deserves a blog post.

Programs instruct (virtual) machines what to do. Programs tell type-checkers what to check. Programs can also tell program verifiers what to check. A (static) program verifier is a little like a type-checker on steroids. Unlike type-checkers, they tend to be complex beasts. ACL2, Jahob, and Spec#, all tame the complexity in different ways.

The approach in Jahob is code reuse. The developers chose to rely heavily on the work of others and innovated mainly in the area of "putting things together".

Spec# divides and conquers, much like Microsoft does in general. They broke down the process of verification into multiple simpler phases and built probably the best engineered program verifier.

The old ACL2 encodes complexity in data rather than code. More specifically Moore (yes, the same guy who did the string matching algorithm) notes that there is no need for verification condition generation if you simply tell a prover the operational semantics of the language you are processing.

It's funny how the oldest tool has the slickest approach (and, probably, the smallest number of developers). Here are some references:

Data Structures in Imperative Languages

2008-12-02T20:58:00.001Z

So in the past few weeks I have realized I don't really know how to write data structures in Java or in any other imperative language for that matter.

The issue is that once one wants follow certain patterns like visitors or immutable classes, lot of code has to be written by hand in a tedious and repetitive fashion.

The reason is that these design decisions affect all the data structures in a similar way: a visitor pattern requires an accept method for each class; equality, hash code, cloning have the same properties over all classes (such as deep cloning); etc.

Code generation does seem like a good path to follow here.

Thanks to a colleague who is an avid UML modeler I had the opportunity to work with classes generated via the Eclipse Modeling Framework (EMF).

So how did I like it? Not too much. There's almost no control over the code being generated as the template is well embedded in the innards of the framework.

No equals method, no hashCode method, no make methods (which create a class from the given attributes). All have to be written by hand - get me out of here!

Hence I went and looked for other technologies.

A colleague of mine Radu developed a light-weight tool for the purpose in question. The class diagram is specified in a custom language similar to grammar description languages. For instance:

BinaryOperator :> Implies, Iff;

tells us that the classes Implies and Iff extend the class BinaryOperator. The code is generated using templates, which are language-ignorant and may access properties of the classes using special keywords.

For instance, \ClassName is expanded to the name of currently processed class and \BaseName to the name of the base class. This enables us to write templates like this:

public class \ClassName extends \BaseName { ....

More details about Radu's tool can be found in this article.

Radu's approach is nice, concise, and more flexible than EMF. The problem is, however, the template language. Very soon I have discovered that there are properties of the classes that are hard to access. Moreover, it's not quite clear how one extends the generated classes with custom code.

Even though tempted to extend the existing tool with constructs of my desire, I decided to look for other existing approaches based on code generation using templates.

Surprisingly enough, little did I find. The most promising is described in a tutorial using the velocity tool. The tutorial can be found here.

The template language is richer, it supports if statements, variables, and other goodies. Theinclude construct, I believe, could be used to extend classes with custom code.

The language is a bit awkward at times, this could probably be overcome by defining some velocity variables. It seems that one would have to write support for navigating the structures describing the class diagrams one wants to support.

All in all, I have a nagging, ominous feeling that I'm missing something. Is it not the case that pretty much every object orient program needs data structures? Isn't there like million papers on UML and/or code generation?

Could someone please point me to a decent tool that would let me generate data structure code using templates driven by class diagrams?

Matthew Parkinson verifies Java. Very brief and inaccurate version.

2008-11-09T19:52:00.003Z

Here are some slides. (His last slide in the first set is ``do David's exercises.'' Obviously, you'll need to know what those were in order to solve them. David's exercises were ``do John's exercises.'' Happy solving!). Here's a summary of the lectures:

Q: How to model abstraction? A: Use uninterpreted functions.
Q: How to use separation logic to verify Java programs? A: Use intuitionistic separation logic because it plays well with garbage collection.
Q: How to deal with inheritance? A: Attach to each method a static spec and a dynamic spec.
Q: How to reason about concurrency? A: Use a mix of separation logic and rely/guarantee reasoning; we'll call it deny/guarantee.

Do you want more? OK, here's one example. The Visitor pattern is used often by people who write compilers. When you write a.f(b, c) you call function f with three parameters. The first one, a is special in two ways: (1) it will be known by the special name this in the body in of the function and its dynamic type is used to decide which of the functions named f will be called; in general, more than one function f may be called by the same statement depending on the value of a. The Visitor pattern is a work-around not having multiple dynamic dispatch aka multimethods. Or, depending where you come from, you might see it as a work-around not having pattern matching. The main tool used by this pattern is (single) dynamic dispatch, so it will also illustrate how to annotate programs that use this feature of Java.

interface Ast { Ast accept(Visitor v); }
class Constant implements Ast {
  int value;
  @Override Ast accept(Visitor v) { return v.visit(this); }
}
class Plus implements Ast {
  Ast left, right;
  @Override Ast accept(Visitor v) { return v.visit(this); }
}

interface Visitor {
  Ast visit(Constant n);
  Ast visit(Plus n);
}

Given this boilerplate we can do something `useful' to the AST.

class ZeroRemover implements Visitor {
  @Override Ast visit(Constant n) { return n.value == 0? null : n; }
  @Override Ast visit(Plus n) {
    n.left = n.left.accept(this);
    n.right = n.right.accept(this);
    if (n.left != null && n.right != null) return n;
    return n.left != null? n.left : n.right;
  }
}

If you are unfamiliar with the Visitor pattern you can spend a few minutes starring at the code above. Or you could continue reading and notice how sprinkling annotations actually helps to understand the code. So, how do we annotate the accept method? If the visitor and the AST node are OK (for some definition of OK depending on the visitor and on the node, respectively), then some value will be returned (for some definition of some, depending on the particular visitor. OK, so we'll just say what we just said.

interface Ast {
  Ast accept(Visitor v)
    requires this.OK(t) ** v.OK(o)
    ensures v.Result(result, this, t, o);
}

``Whooooaa, stop! What's the funny **, and what are t and o? You said you'll write exactly what you said!'' Uhm, the stars are just the separating conjunction; we use two because one is taken by multiplication. The t and o is just stuff, uninterpreted for now if you want. We're just saying that the Result may depend on the state of the node and on the state of the visitor. Feel better? Yes? OK, then let's move on, it's late. I'll skip some specs so we can move quickly to the next interesting bit. How do we say what ZeroRemover is supposed to do? We just provide a definition for the Result predicate, which was uninterpreted (or `abstract') until now.

class ZeroRemover implements Visitor {
  spec
    Result(r, a, t, o) = r == rz(t);
    plus(Constant(0), x) = x;
    plus(x, Constant(0)) = x;
    plus(x, y) = Plus(x, y);
    rz(Plus(x, y)) = plus(rz(x), rz(y));
    rz(x) = x;

  @Override Ast visit(Constant n) { return n.value == 0? null : n; }
  @Override Ast visit(Plus n) {
    n.left = n.left.accept(this);
    n.right = n.right.accept(this);
    if (n.left != null && n.right != null) return n;
    return n.left != null? n.left : n.right;
  }
}

Let's recap: In the specs you write a Haskell program that does the same thing but is shorter and (perhaps) slower and also some bridges between Haskell (aka math) and your program. As a result you can run a tool to tell you if your efficient(?) Java program does the same thing as the Haskell one.

Now, can you fill in the specs that I skipped? If not, then please do ask in the comments what information you feel you are missing.

Separation logic

2008-11-09T16:50:00.001Z

A good way to learn separation logic is to read Reynold’s introductory lecture notes. This is a little bit like saying that a good way to learn programming is to read Knuth’s books. If you are the type of person that likes using iPhones and searching with Google you might need a bit more to wet your appetite.

Separation logic was designed to allow local reasoning. ‘Local’ is a generalization of ‘modular’. You can say ‘local’ when you have some sort of distance and you can say “a is close to b but far from c.” We reason locally when all the stuff that we need to keep in our head at one time is ‘close’. ‘Modular’ is simply ‘local’ specialized with program text distance. The typical distance people have in mind when they talk separation logic is “the number of pointer indirections I need to do to get from location x to location y.” When you think about a linked list you tend to ignore other linked lists that are at distance ∞. Good, so the central concept of separation logic is locality; or separation, depending on how you look at it.

A logic is a very simple language with very precise semantics. To describe the logic (that is, the one most people know) you need to introduce operators and describe what they mean (for example, p ∧ q evaluates to ⊤ when both p and q evaluate to ⊤); in other words, you introduce a piece of syntax and then you give its semantics. Thinking in terms of semantics is not always efficient. Sometimes you need to get in the symbol crunching mood. That’s why you’d typically present rules for manipulating symbols that are sound (for example, p ∧ (q ∨ r) can be replaced by (p ∧ q) ∨ (p ∧ r)).

There are three pieces of syntax that are new in separation logic: the separating conjunction p ⋆ q, the points-to operator x → v, the separating implication aka the magic wand p −⋆ q, and emp. The semantics are described in terms of a somewhat more complicated model. Now we have not only booleans plus some abstract domain. Still, the model will be familiar to any programmer. We have addresses, values, a stack (inappropriately named ‘store’ by the old-timer Reynolds), and a heap. (BTW, there’s nothing wrong with ‘store’ per se. It’s just that most programmers prefer the ambiguous terms ‘stack’ and ‘heap’.) So,

p ⋆ q holds in a heap that can be split in a part where p holds and a part where q holds,
x → v holds in a heap that has exactly one cell whose address is x and whose content is v,
p −⋆ q holds in a heap that can be extended with a heap where p holds to get a heap where q holds,
emp holds when the heap is empty.

Once we introduce these new operators we also get new laws, such as:

p₁ ⇒ p₂ and q₁ ⇒ q₂ can be replaced by p₁ ⋆ q₁ ⇒ p₂ ⋆ q₂
p₁ ⋆ p₂ ⇒ p₃ can be replaced by p₁ ⇒ (p₂ −⋆ p₃)

In fact there are classes of assertions for which extra rules can be used.

pure assertions are those that don’t say anything about the heap so they can be pulled out of the new operators; for example (p ∧ q) ⋆ r can be replaced by p ∧ (q ⋆ r) if p is pure,
strictly exact assertions are those that uniquely identify the heap,
precise assertions are those that identify a unique subheap
intuitionistic assertions are those that hold for any extended heap
supported assertions are those for which there is a least subheap on which they hold

Now we can annotate programs with descriptions of the state at various intermediate points. If we also have rules on how the state is changed by simple commands we can then derive formal proofs of programs, meaning that the annotations can be shown to agree with the program by pure ‘symbol crunching’, something even a computer should be able to do. People who write such programs have a knack for funny names: Space Invader and Smallfoot. Well, perhaps not all people who write such tools. There is also the Unnamed and Unreleased tool from Matthew Parkinson that handles Java code. Edit: Matthew pointed out that the tool has a name: jStar. (Please write a comment if another tool should be mentioned here.)

The interesting algorithms proved correct (in the sense explained above) using separation logic are Schorr–Waite and Michael’s stack. (Please write a comment if another algorithm should be mentioned here.)

Let me briefly present these two algorithms.

The Schorr –Waite algorithm is used to reduce memory usage during garbage collection. For our purposes ‘garbage collection’ simply means that we want to mark all reachable nodes from a given root. The simple solution is to do a DFS. A simple implementation would use a stack of pointers that may grow in the worst case to be linear in the number of nodes in the graph. The trick Schorr and Waite use is to use the link fields in the graph to store the backpointers.

Michael’s stack is lock-free and works in the presence of memory reclamation. You want to implement push(stack, node) and pop(stack), where stack is a pointer identifying the stack. These functions will be used from multiple threads and the only synchronization primitive you are allowed to use is the compare-and-swap statement. To push a node you would probably try to read stack->next, set node->next := stack->next, if stack->next == what I read then set stack->next := node. The last operation is the compare-and-swap: “If the first element of the stack is still what it was when we looked the first time then make node the new first element.” The problem with this is that “the same first element” doesn’t necessarily mean “the next pointer of the first element is the same.” No one is supposed to change the next pointer apart from push and pop, but it may very well be that the node is freed, a ‘new’ allocated node happens to be the same area in memory and then there is nothing holding back the change of the next field. That is, unless you use an array of stuff that shouldn’t be touched, as in the solution given by Michael.

That’s it for now. Oh, and sorry if you were under the impression that I’m trying to ‘wet your appetite’. I was merely trying to draw a child’s sketch of separation logic.

FIRST Fall School

2008-11-09T14:02:00.002Z

At the end of last month I attended (as a student) the FIRST fall school on the logics and semantics of state. John Reynolds told us about separation logic. David Nauman and Matthew Parkinson showed us various approaches to verifying object-oriented programs. Zhong Shao outlined a project whose vision is to verify a simple operating system. Finally, Lars Birkedal and Hongseok Yang talked about some really abstract math.

Reynold's lectures were thorough and clear. Parkinson's were fun and accessible. My lack of knowledge made it difficult for me to follow closely the other lectures so I hesitate to attach adjectives to them. But I do recommend you miss no opportunity of having Reynolds or Parkinson as a speaker in your university (or company).

I'll follow up with a few posts to outline what I learned.

Don Batory on Category Theory in SPL and MDE

2008-10-30T14:14:00.004Z

At MODELS 2008 Don Batory gave a talk on how category theory relates to Software Product Lines (SPL) and to Model Driven Engineering (MDE). There's a good paper covering most of the talk so I won't go into much detail here. But let me try to convey the aspects I found the most interesting.

I don't want to pretend I know much about category theory but I believe that one doesn't need to know much more than that it is a bunch of points and a bunch of arrows between them to dig what Don has on his mind (let's see how many categorists read this).

MDE is about refinement: going from highly abstract models, one gradually gets to an implementation via models with increasing level of refinement. Don presented an example of a process which derives Bytecode from a DSL via a more specific DSL and Java code. So here we got:

DSL₁ → DSL₂ → Java → Bytecode

Now to get a category, consider program representations as points and transformations as arrows between them. Note that identity transformations and composition of transformations exist. However non-groundbreaking this might seem at first sight, it is important to realize that such diagram is an important concept in MDE and it might be worth including such as an artifact in software development (the paper points to relevant work on megamodels and on tool chain diagrams).

Ok, MDE development chain is a category, now what about SPL? A software product line is a means of developing and maintaining a family of similar software artifacts (typically programs). As reuse is the key, these family members are compositions of features (some might want to call them aspects at the software level).

So where's the category hidden in this setup? Imagine programs of a product line as points and features as arrows between them. So a feature is a delta adding functionality to a program which gets us to another program.

As a particular software product line considers only certain compositions of features, a feature model is used to determine which compositions of features, also known as arrows, are valid (or are considered if you wish).

Now this really gets groovy if we combine MDE (refinement) and SPL (program synthesis). Imagine you got a software product line which we want to refine into another product line. Categorically speaking, we need to transform not only points to points but also arrows to arrows — features of the first product line to the features of the more refined one. In effect, a product-line is a directed graph (category), and what we are doing in refining a product line is mapping a directed graph (category) to another directed graph (category).

So let's say we have a product line S in which the program s₁ is mapped to the program s₂ by the feature f_S. Further, the product line S is refined to a product line B in which b₁ is mapped to b₂ by f_B. Now if we know that b₁ is a refinement of s₁ and b₂ a refinement of s₂, we obtain the following arrows:

The cool think is that this should commute: If I want to get from s₁ to b₂, I can either go via b₂ and use →_{f_B} or, I can go to s₂ via →_{f_S} and then refine to b₂. If the term commuting diagram popped out in your head, it's not by accident (if it hasn't, the diagram above is a commuting diagram).

How's that useful? Don describes two scenarios, one when testing (verifying) this commutativity led to a discovery of bugs in his software and one where taking one route was computationally more efficient than taking the other. So the morale is: "Look for commuting diagrams."

To conclude let me advertise my own work (done with Goetz Botterweck), which investigates the refinement of feature models and I think it would be interesting to investigate how it relates to the concepts by Don. And I encourage anyone who's dabbling or working with Software Engineering to read this article as it's a fruitful ground for ideas and one doesn't need to be scared of math as there's only little of it.

Jeff Kramer on Abstraction

2008-10-13T12:47:00.001+01:00

Here are some notes that I've taken down from a keynote speech given by Jeff Kramer at MODELS 2008. The keynote was about how and if to teach abstraction and how abstraction is important for SW development and design. Some students just do not understand clearly certain concepts (concurrent algorithms, modeling) whereas some students are really good. What is the difference between the good and unable students. The answer is abstraction. What is abstraction?

remove detail (simplify) and focus (selection)
finding commonalities

Jeff exemplified abstraction on metro maps. London was the first one to use abstraction to depict the routes, i.e., not adhering to the geographical parameters. Metro maps around the world use this abstraction now. One should keep in mind that each abstraction is fit only for certain purpose. Don't use the abstract metro map instead of a normal map when you are walking around the city. Software is abstract, intangible, by its nature. Hence abstraction is important in its design. This leads us to the following Question: How do we obtain the skill of abstraction? Can we teach that? Answer: It's part of our genes but, no doubt, can be improved by teaching. According to Jean Piaget's cognitive stages, abstractions skills develop between the age of 12 and adulthood. Bad news: abstraction skills reached only by 30% of people. What do we do to improve this?

teach enough mathematics
teach modeling and analysis, must be tool supported, students must feel the benefit

In the second half of the presentation, Jeff gave a demo of some examples and tools that he's using in his course on concurrent systems. A formal language is used to describe concurrent systems and these can be further analyzed, animated, etc. in a LTS Analyzer. See Jeff's book for more information. An example that I found interesting was how to use deadlock detection to solve the Fifteen puzzle. And a small problem at the end. Let's have the famous N dining philosophers problem. An even-numbered philosopher will always first pick the fork on the left and then the right one whenever he wants to eat. An odd-numbered philosopher will pick the one on the right first. By picking I mean that the philosopher waits if the fork is in use. For which N this strategy does not deadlock?

Job Openings at Kind Software group in UCD

2008-03-05T23:04:00.001Z

We have one open position for a Ph.D. student and two open positions for research software and hardware engineers at the Kind Software research group in University College Dublin.

(1) Research Hardware Engineer in Dependable Scientific Computing (2) Research Software Engineer in Dependable Scientific Computing (3) PhD Student in Applied Formal Methods

within the group

KindSoftware: Software Engineering with Applied Formal Methods A part of the Systems Research Group, a member of the CASL: Complex & Adaptive Systems Laboratory, within the School of Computer Science and Informatics, at University College Dublin.

All positions report to Dr. Joe Kiniry.

Research Software and Hardware Engineers

Research Engineer candidates should have a M.Sc. in Computer Science, an appropriate Engineering degree, or Mathematics (or equivalent) and an established software engineering record. Experience in more than a few of the following fields is mandatory:

Java 1.5 expertise
the Eclipse Platform and IDE
system analysis and design with semantically meaningful specification languages (i.e., not UML)
unit, integration, and system testing with automated and manual test frameworks
design by contract
the Java Modeling Language (JML) and its tool suite
ESC/Java2
FLOSS licenses, development styles, and technologies
quality functional languages (ML variants, Haskell, Clean, etc.) and object-oriented languages (Eiffel, Smalltalk/Squeak, Ruby, etc.)
the expert use of debuggers like jSwat and profilers like jProfiler
XML-based technologies
sensor hardware and software systems
large-scale (multi-terabyte) datastores, particularly iSCSI-based SANs and similar
installing and maintaining compute server farms running various flavors of Linux, Solaris, and OS X

Ph.D. students:

We are seeking very well qualified graduates, or students expecting to graduate in the near future, to undertake selected projects in the broad area of Applied Formal Methods. These students will play a pivotal role in developing our research profile and will be involved in every aspect of the foundation of the research group.

Our ideal candidates will be able to demonstrate an ability to both undertake basic research in Computer Science and Mathematics and be able to build prototype systems to demonstrate their research.

The candidates will be expected to work in collaboration with a number of internationally known existing groups at other top institutions including: INRIA, ETH Zurich, Radboud University Nijmegen, Ludwig-Maximilian University in Munich, the University of Edinburgh, the Chalmers University of Technology, Imperial College London, Warsaw University, the Technical University of Madrid, and at companies like France Telecom and SAP. Our group also collaborates with a number of other top-notch universities and companies in the U.S.A., Canada, Australia, and New Zealand including MIT, Caltech, Kansas State University, the University of Washington, and others.

Applicants for Ph.D. positions should have achieved at a first (or equivalent) in Computer Science and have a keen interest in research.

Applicants should return a completed application form with referee reports CV to Joseph Kiniry at the address below. Informal inquiries prior a full application are welcomed.

The application form is available via the Research Degrees section of the School website.

About the School

The Irish Government (SFI/Forfas) Baseline Study that ranked Irish research groups identified the School of Computer Science and Informatics at University College Dublin as the best Computer Science department in the country, having "a very strong impact internationally in their research." This research excellence is further reflected in the large number of prestigious Science Foundation Ireland (SFI) funded projects won by members of the School.

Contact Information

Please contact Dr. Joe Kiniry for further details of the above posts.

This work is funded under an EU FP6 Global Computing II Grant: MOBIUS and SFI grant "The CASL SenseTile System".

JML Winter School 2008

2008-02-28T12:59:00.000Z

The first JML Winter School was held in Orlando, Florida on 23-24 February 2008.

The first day of the tutorial was devoted to showing how to get the Jikes Parser Generator working with JML4 and a simple example of how to generate bytecode for runtime assertation checking (RAC) by extending the Eclipse JDT. The second day was a more in-depth example using loop variants and loop invariants.

JML4 will be based on the next version of Eclipse e.g. 3.4 and will support Java 1.5, unlike previous generation JML tools.

SAVCBS, FroCoS, and FTP: A trip report

2007-09-18T16:32:00.000+01:00

Post by Radu Grigore:

I spent the last couple of weeks attending three workshops: SAVCBS, FroCoS, and FTP. The keyword for SAVCBS is components. Many people in the program committee, however, are formal methods people. Both FroCoS and FTP are about theorem proving. FroCoS is focusing on integration. Many articles were about how to put together interactive and automatic theorem provers. FTP is less popular and may even disappear. As I understand, historically the papers were very theory oriented and that is why more applied people are reluctant to submit papers. Although the program committee is made out of theory people they seem to be open to applications. If you are working on a theorem prover or if you are using a theorem prover have a look at future editions of this workshop.

The following is a selection of my notes. It includes details only for presentations that were either particularly clear or related to my work.

1 SAVCBS

Short papers first. These have really preliminary results. In fact, some can be viewed as position papers.

Specification of trustworthy real-time reactive systems. This is a paper about design methodology. It seems to be similar to what Vali and Oana are doing, but it is not my cup of tea. The basic idea is to have a formal specification of the requirements, generate automata from them, and model check them. It sounds a bit like magic.

Component, objects, and contracts. The goal here is to design a (formal) language able to express the kind of things that appear in legal contracts. Also, the authors would like to treat legal contracts like components, but it is unclear why and how. The language and its semantics would be quite cool in my opinion. It could be used, for example, to teach computer scientists how to read all that legal gibberish.

A concept for dynamic wiring of components. The idea is to introduce some kind of behavioural subtyping. This implies a specification language and tools to check for subtyping. The goal is to statically determine if it's safe to change a component with another one. I pointed out that in previous work on dynamic upgrade state was a major problem that seems to be completely neglected. (Remember that this is preliminary work.)

Game-based safety checking with Mage. The presentation was very thin (aka `high-level') and full of cute pictures. (People who know me can infer from that that I could barely stay in the room.)

The next papers were supposed to present results that are have some technical meat.

Effective verification of systems with a dynamic number of components. First of all, the title is misleading. The paper is not about plugging in and out components in a working system. Instead, it introduces a temporal logic that can be used to reason about classes of (transition) systems parametrized by the number of components. I didn't quite get what's the point.

Plan-directed architectural change for autonomous systems. In my opinion the presentation was particularly bad and managed to obscure a lot of what seemed good work. All I got is that a plan seems to be something like a very high-level program that can be used, for example, to guide a robot.

Reachability analysis for annotated code. Mikoláš's presentation went well. I'll have a series of posts about reachability on my blog.

Faithful mapping of model classes to mathematical structures. This talk by Ádám Darvas was very good. For a brief description I shall again refer you to my blog. I'll just say here that I highly recommend JML people to read this article.

Proof transforming compilation of programs with abrupt termination. This presentation contained some cute Java quizzes that stumped both me and Mikoláš. Here's the question I got wrong: What does the following program do for the call f(1)?

static int f(int x) throws Exception {
   int r = 0;
   while (true) try {
     if (x > 0) { throw new Exception();  }
   } finally { ++r; break; }
   ++r;
   return r;
}

The article presents some formal Java semantics that capture the interplay of the try ⋯ finally, break, and while constructs. Moreover, it discusses a bit how to transform proofs about such programs at source level into proofs at bytecode level. Again, all JML people should read this article.

Playing with time in publish-subscribe using a domain specific model checker. I couldn't follow the details of this presentation. The message seemed to be that they customized the model checker Bogor to more efficiently deal with a bunch of components communicating using a publish-subscribe bus.

On timed components and their abstraction. I am a fan of covering the basics in a presentation but this guy went over board by only covering what timed automata are.

2 FroCoS

I'll start with the invited talks. These generally cover a lot of ground and give a historical perspective on a whole specialized area. The presenter is one of the key people in that area but does not restrict himself (or herself) to his (or her) own work.

From KSAT to delayed theory combination: Exploiting DPLL outside the SAT domain. SAT solvers are very good. That's why many people transform their problems in satisfiability problems and then use a SAT solver. Three particular places where this was done is in reasoning in modal logics, in writing Satisfiability Modulo Theories (SMT) solvers, and in writing SMT solvers for combined theories. The talk was given by one of the MathSAT people.

In modal logics the basic algorithm is to use the SAT solver to find a model, check its consistency with the modal logic (by using tableux rules), rinse and repeat. Essentially the SAT solver is used to enumerate models (assignments of values to constants) in an organized way.

Something very similar happens in SMT provers. The SAT solver finds a model, a decision procedure checks if that is consistent with the theory and if not gives an explanation, rinse and repeat. It's hard to write a decision procedure (that is correct) for a big theory. That's why people prefer to write decision procedures for fragments of the theory and combine them. Nelson–Oppen is the traditional way of doing so. The facts exchanged by decision procedures are equalities. In delayed theory combination (DTC) the SAT solver is used to manage the communication between decision procedures thru booleans.

Architecting solvers for Satisfiability Modulo Theories: Nelson–Oppen with DPLL. A formal description of the architecture of SMT solvers has good educative value (it made things much clearer for me!) and it can used to reason about the solver. These guys at Intel described their SMT solver as a set of rules that can be interpreted. They also used Isabelle to prove various properties of the rules. Of course, the interpreted version is way to slow. They are implementing the `real' thing in OCaml and they will release it on SourceForge in the coming months. The intended application area includes hardware verification, embedded systems verification, device drivers verification.

I highly recommend this paper, for example, to those who want to understand the essence of Nelson–Oppen or who want to start working on a (possibly existing) SMT solver.

Temporalising logics: 15 years after. This talk was much too theoretical for me. All I could understand is that adding time to various logics puts the satisfiability problem in various classes of (huge) complexity. My impression is that in a SMT solver anything quadratic is already dubious. Something whose complexity is given by the Ackermann function is ridiculous. Anyway, I'm happy someone (else) is looking into these fundamental issues.

Those where all the FroCoS-pure invited talks. Now let's move on to the normal presentations.

Visibly pushdown languages and term rewriting. This is a study of a certain set of (tree-accepting) automata.

A compressing translation from propositional resolution to natural deduction. This work tackles a specific problem that appears in integrating automated and interactive theorem provers. A SAT solver can give a resolution proof that a formula is UNSAT. An interactive theorem prover usually has a small proof checking engine. Everything goes thru there. It would be a bit strange to use externally a SAT solver, which is a big chunk of C code, without running its result thru the trusted kernel. But proof checkers are usually designed to handle proofs by natural deduction. (This basically means that the proof is a tree whose structure around each node matches one of the given rules.) This paper presents an efficient way of solving the impedance mismatch. Checking the proof still takes longer than finding it, so there is room for improvement. But I will definitely read this article carefully because it uses Generalized Suffix Trees applied to theorem proving!

Combining algorithms for deciding knowledge in security protocols. I think it was about how to combine equational theories.

RoCTL: A temporal logic of robustness. These guys added two operators to CTL so that you can say ◯φ (in all possible futures φ holds) and ▴φ (in all futures with one more failure φ holds). A problem posed by the presenter is whether RoCTL is elementary. Here is an example to give you an idea of what can be easily expressed in this logic: “You must help your neighbor. If you will not help your neighbor you have to warn him.” (The guys who presented Components, objects, and contracts at SAVCBS should probably take a look at RoCTL.)

Temporal logics with capacity constraints. This was a rather practical presentation that I enjoyed. If you want to say in LTL that ≤2 of a₁, a₂, a₃, a₄ are true then you can add some syntactic sugar and then use (¬ a₁∧¬ a₂) ∨(¬ a₁∨¬ a₃)∨⋯ to do the verification. The problem is that in practice this doesn't work. You need to put the treatment of such constraints in the model checker. They presented an algorithm (but not an implementation!) of how to do so. I just hate when I hear that “we just need a student to implement it.” Let me remind you that SOFTWARE IS HARD.

Languages modulo normalisation. No idea what this was about.

Combining classical and intuitionistic implications. The talk was about finding axioms to add to the classical and intuitionistic axioms such that deduction theorems still hold and such that classical and intuitionistic implications remain essentially distinct operations. Then it continued with how to find models for a logic given by such a set of axioms.

Proving termination using recursive path orders and SAT solving. I'd say that the presenter, Peter Schneider-Kamp, is a hacker (the good kind). He is working on an automated program verification environment (AProVE). At this point AProVE tests whether programs terminate or not. You can go ahead and type in a Haskell program in the web-interface and see what happens. It's quite impressive. The overall idea is to translate the program into a term rewriting system (TRS) which terminates iff the program terminates. Then the TRS is analyzed using some fancy techniques that I do not (yet) understand. The talk was about an improvement of these fancy techniques that makes the tool a lot faster.

The good news is that they are considering using BoogiePL as input in order to handle imperative programs and I'm developing an open source front-end for that language. I'd be quite happy if they will be my users.

Notherianity and combination problems. I believe this was about extending Nelson–Oppen to the case where theories are not disjoint, but obey some more general constraint called `notherianity'.

3 FroCoS and FTP

The joint session of FroCoS and FTP had one invited talk and three normal talks. Let's start with the invited one.

Hierarchical and modular reasoning in complex theories: The case of local theory extension. The message of this talk for me was that in theory it is possible to organize some theories (pun intended) into a hierarchical structure and use that hierarchical structure to guide the instantiations in a SMT solver. The really nice part is that you can guarantee completeness with such an approach. (Sounds like a nice experiment for Michał).

Now the regular presentations.

Combining proof producing decision procedures. This paper formalizes (part of) what is done in SMT solvers nowadays. The main result is a data structure, the explanation graph, that can be returned by decision procedures instead of conflict sets. This data structure has nice compositionality properties and ensures some kind of minimality (which might not work well in practice for all we know). I have an idea of how this data structure could be slightly improved (and I told Cristophe Ringeissen about it). I'll have to investigate if it works.

Towards an automatic analysis of web service security. It must be my dislike of `new technologies' that put me to sleep during this presentation. Apologies.

Certification of automated theorem proofs. Coccinelle is a Coq library for expressing termination problems. CiME is a program that tries to find termination proofs that was enhanced to produce proofs expressed in Coccinelle that can be checked by Coq. Checking the proof takes about four times as much time as producing the proofs and the presenter said this is `normal' and that doing the proof check with something else than Coq would not help. I wonder if he'll be surprised when Michał will finally publish what he did here.

4 FTP

The invited talks.

The KeY tool. Unfortunately I missed the first half of this talk. The KeY tool translates Java programs into a complicated logic. The first step is to do symbolic execution. The result of this is that all strange constructs in the logic are eliminated and what remains is first-order logic. This sounds a lot like VC generation, except that I got the impression that it is more interactive. For example, the user can say if a method call should be handled by inlining the body of the method or by using the method's spec. In fact, one of the main ideas held by the presenter is that “interaction is important to handle complex programs.” The presentation then went on to cover one way of integrating interactive and automated theorem provers. In this setting automated theorem provers are trusted (without checking).

Applying first-order theorem provers in formal software safety certification. At NASA people have problems that are hard to express in C. It's much easier to design a domain specific language (DSL) that physicists and mathematicians can use so that their bugs don't need to wait for the postdoc implementing in C telling the researcher that their algorithm is crap. Using a DSL keeps postdocs out of the loop and researchers can work at high-level with the computer to ensure that their ideas are correct. Now, a compiler for a DSL that outputs C code (in a subset of the language) is a huge beast and it is quite difficult to ensure that it is correct. So, the next best thing is to verify that the produced programs (one by one) have a set of desired properties (also checked one by one). What they did is very similar to ESC/Java with three differences:

the annotations are generated from DSL (like the code)
properties are generated one by one (like producing a VC for checking that null pointers are not dereferenced, one for checking that there is no out-of-bounds array access, etc.)
the theorem prover they used is resolution-based (Vampire)

The lessons they've learned show (mostly) that they should have used an SMT prover instead of Vampire:

The prover is not wrong. Bugs are usually elsewhere.
TPTP ≠ Real World.
Need controlled simplification. Doing some simple simplifications (!) before starting the actual proof goes a long way.
Need axiom selection. (hint, hint: We have a huge background predicate. Also, Georg used the same trick when playing with Kleene algebras. See below.)
Need built-in theory support.

Now the normal talks.

Induction in sequent calculus modulo. Didn't understand anything.

Extending Poitin to handle explicit quantification. This presentation was given by someone from Dublin City University (!). Unfortunately, all I could understand is that they are using program transformation to do interactive theorem proving. Somehow.

Developing modal tableaux and resolution methods via first-order resolution. This talk was over my head. The presenter talked about how to find deduction calculi for modal logics.

Reasoning automatically about termination and refinement. This was a really nice talk. It started from the Bachmair-Dershowitz theorem: “Termination of the union of two rewrite systems can be separated into termination of the individual systems if one rewrite system quasicommutes over the other.” This can be proven for more general (abstract) structures than TRSs. The presenter managed to give an ugly proof a few years ago that this theorem applies to Kleene algebras. Now he used an automated theorem prover and managed to extract a much nicer proof. His work consistent of playing with adding and removing known results about Kleene algebras as axioms. Too many axioms made the theorem prover diverge, too few made it provide counterexamples. Also, he showed that Kleene modules are better candidates because, appart from the informal motivation, the theorem prover was able to derive the said theorem without him doing anything. (PS: Kleene algebras are structures introduced by the Conway.)

Proof Builder. This was a system presentation. ProofBuilder is a tool used to teach students what a proof is. It was designed so that the styles in common Discrete Mathematics textbooks are covered.

Labeled tableaux for distributed temporal logic. DTL is a logic meant to be used to reason about properties of security protocols. Existing arguments in this logic are semantic based. The contribution is a calculus (for a subset of the logic used in practice) and an algorithm (based on Bellman-Ford) to extract models. It is unknown if DTL is decidable.

What first-order theorem provers do for monodic temporal logic. The presentation Ullrich gave was great for someone like me. First-order temporal logic (FOTL) is not semi-decidable. (There is no complete axiomatization of it.) So theoreticians try to find interesting fragments. The one presented has a restriction of the number of free variables that can appear under temporal operators (at most one). They proved that everything can be put in a certain normal form and that resolution is sound and complete. The architecture of the prover is waiting for an implementation.

A graph-based strategy for the selection of hypotheses. These guys assume that the theorem prover query has a specific form. (It is not yet clear to me how important this restriction is.) Then they construct some dependency graphs that lead to a heuristic ordering of how relevant are `hypotheses' for proving the `goals'. Here `hypotheses' and `goals' have a specific meaning related to the specific form I mentioned above. Then they try to prove the goal using only the most relevant hypotheses, and gradually keep adding hypotheses if needed. The idea is that this process might succeed where the naive technique of always using all hypothesis might diverge. Again, I don't know what is the impact on performance. The idea, however, is quite powerful in handling really hard verification conditions. (Maybe this kind of things should be included in the theorem prover.)

Redundancy in the geometric resolution calculus. Skolem was interested in geometry, which explains the historical name of this calculus. The idea is that if logical formulas are restricted in a certain way reasoning can be done differently. In fact this was the motivation of the presenter: let's try something new. As I understand, the approach is reasonably good at producing models, but not that good at finding proofs.

Edit and Verify. I was unhappy with my presentation. Anyway, Silvio Ranise gave me a cool idea of how to apply this stuff. More details about what Edit and Verify is will follow on my blog. In the meantime you can have a look at the paper.

Dagstuhl Seminar Panel: Science, Policy, the Press, and Politics

2007-08-19T10:34:00.000+01:00

Rop Gonggrijp and I proposed a panel session we ran on the first afternoon at the recent e-voting Dagstuhl seminar on the relationship between science and policy, the press, and politics. The other people on the panel, besides Rop and I, were J. Alex Halderman, Dan Wallach, and a member of the German press that was attending this event, Richard Sietmann. The main point of the panel was to emphasize to the audience that scientific work in this area cannot be divorced from politics and we also offered many war stories and advice on interacting with government, vendors, and the media. My main recommendation was that every scientist that is doing research that has potential media interest should read "A Scientist's Guide to Talking with the Media" by Richard Hayes and Daniel Grossman. I have found this book invaluable. It has informed my interactions with not only the media, but also with the general public, and even other experts. Clearly communicating the core of complex ideas, like those inherent in the "hot" topics of e-voting or applied formal methods, is critical. It is an added bonus when you can combine the disciplines, as convincing computer scientists of the use and utility of modern applied formal methods is just as hard as educating government ministers of the dangers of currently available commercial e-voting computers, but for entirely different reasons. I am encouraged by young researcher/activists like Alex and Dan. The world needs more activist scientists. These Ph.D. students and young not-yet-tenured professors are very brave to grab the e-voting bull by the horns, and I'm proud of them for that. Perhaps the generational apathy of the past 20 years can, in some small way, be counteracted by the all-consuming passion of the modern hacker/scientist? I know I'll keep making a fuss.

2007 Electronic Voting Technology Workshop

2007-08-17T22:40:00.001+01:00

Last week I was presenting a paper at EVT07. Here are my notes/observations. 2007 USENIX/ACCURATE Electronic Voting Technology Workshop (http://www.usenix.org/events/evt07/tech/) 6th August: EVT Session Analysis I: First talk of the day was a talk from the Dutch group "We don't trust voting computers". This a well presented talk with video clips showing how easy it was to change the EEPROM on a voting computer, in 60 seconds, and of reprogrammed voting machine which could play chess. The second talk was similar, but was about Diebold machines in the US. The lock can be picked in less than 10 seconds. The third talk was about issues with technologies for disabled voters, namely the DV eSlate (http://evote.cs.ucdavis.edu/). All three types of voting machines have radio emissions from raster displays, which can be detected and analyzed. EVT Session Design I: The first talk showed how to use hash chains to prevent/detect tampering with an audit log. This assumes that the information in the audit log can safely be made public (in encrypted form) and then shared between servers for redundancy. The second talk was about how to reduce the complexity of voting machine software by pre-rendering the user interface. My talk about verification of electronic vote counting for PRSTV was before last before lunch. This was the only paper at EVT to discuss formal methods, with mixed reaction. Several cryptographers suggested that a list of votes cast could be made public (in encrypted form) to allow each candidate/party to count the votes for themselves. I was asked to explain PRSTV in more detail. Also, some cryptographers suggested that is better to verify the result with independent counts rather than to verify the count process or the software. However, I don't know of any existing cryptographic schemes which work well with PRSTV from a vote counting perspective. At present in the paper based system, ballots are not made public, only the number of votes held by each candidate in each round and the proportion of transfers in each round. It was suggested that randomization, which is part of PSTRV, could be done in advance with a predefined table of random numbers. However, this could compromise the anonymity of the votes. So, I still think that the actual vote counting process needs to be formally verified. EVT Session Auditing and Transparency: The first talk of this session described the confidentially requirements of contracts between voting machine vendors and election agencies in the US, which prohibit almost all use/analysis of the voting machines/software, except where necessary for the purpose of casting a vote. Also, the contracts are confidential. In some cases the audit logs are confidential. Some vendors to reserve the right to update the election software at any time e.g. just before an election. The second talk of the session described how to calculate the optimal sample size for auditing. The next talk described how to automate the auditing of ballots (http://itpolicy.princeton.edu/voting). The last talk of the session described an experiment in which college students were unable to successfully complete an audit that required recounting of VVPAT (voter verified paper audit trail) receipts, meaning that VVPAT receipts need to be redesigned for usability. EVT Session Analysis II: The first talk of this session described a software tool called Pioneer, which is designed to run on voting machines, checking that none of the software runs slower than expected. The idea is that if the software is compromised or acting maliciously, then it will take longer, than it should, to perform certain calculations. The next paper described a ballot layout attack against optical scan vote terminals; candidate name indexes can be swapped in memory, but the VVPAT receipt will appear to be correct. The last paper of this session showed how voting certification standards discourage good database design by requiring additional documentation if the design is more secure. The data model for GEMS, which is the Election Management Software used by Diebold, does not even comply with first normal form. Different parts of the tally get stored in different parts of the database. It has been shown to give inconsistent reporting of election results i.e. count the same set of votes on two different days and get two different results! Negative numbers of votes were stored in some parts of the database. Microsoft JET was used as as the database engine, although it does not guarantee "absolute data integrity". Law professor Candice Hoke, makes the point that the legislation needs to specify some minimum set of technical/quality standards e.g. database schema must be at least as good as 2NF, or equivalent. How best to express these technical standards in legal form is an open question. EVT Session Design II: The first talk proposed a scheme whereby a voter using a direct recording (DRE) voting machine can choose either to cast the vote as normal or to challenge the machine to decrypt the vote correctly, just by adding one question to the voting process. The next paper described a more complex scheme with two half-receipts for each vote. The voter retains one half-receipt; enough to verify the vote, not enough to reveal the vote. The last talk described three different non-cryptographic schemes: Three Ballot (which would not work with PRSTV), VAV (Vote, Anti-Vote, Vote) and Twin. Although VAV might work with PRSTV, it has some usability issues i.e. the need to fill out the ballot paper three times. See also: http://benlog.com/articles/2007/08/06/electronic-voting-technology-2007/ ===== USENIX Security 07 Technical Sessions (http://www.usenix.org/events/sec07/tech/tech.html) 8-10th August: Web Security Session: First talk was about SIF (servlets with information flow) which is based on JIF. Next talk was about using tokens to weight the value of clicks on a syndication site. Then a talk about execution based analysis of untrusted websites using a kind of virtual machine. Privacy Session: The privacy session described how variable bit rate encoding, which leads to more efficient packet sizes can also leak data, so that encryption is not enough. The second talk of that session applied the same analysis to pervasive computing devices. The third talk described how to infer data from anonymised documents e.g. most people can be identified just by their gender, date of birth and ZIP code. Authentication Session: Very interesting talk about relay attacks on smartcard payment systems, including a video clip from BBC TV programme 'Watchdog' and a proposed solution using distance bounding. The next talk showed techniques that be used to discover graphical passwords by finding hot spots in images.. The third talk was a way of encoding a user-specified time delay into offline passwords so as to make dictionary attacks about 3.59 times harder. Threats Session: Two talks about spam and one about botnets. The first talk about using image shingling on screenhots to profile the 'scam' sites. The second talk about establishing IP reputation so that overloaded mail servers could bias towards legitimate mail senders. The third talk was about a BotHunter tool for detecting bots i.e. remote controlled malware. Analysis Session: The analysis session included a talk on integrity checking of cryptographic file systems, and a talk on reverse engineering of message protocols. The last talk in that section, awarded 'best' in conference was about detecting variations in different implementations of the same protocol e.g. two different HTTP servers. This was done by extracting symbolic logic from the binaries (assembly code) using an intermediate language and weakest precondition analysis and then finding a set of inputs for which the two implementations differ. This could be used either to find error conditions or to fingerprint the binary executables. Invited Talks on Electronic Voting: There were two invited talks on Computer Security and Voting. The first was a general introduction to the topic by David Dill and the second was a discussion by David Wagner and others of their review of electronic voting machines in California. After the first talk, someone asked a question about randomisation in PR-STV, is used in Cambridge, MA, for city elections. In the second talk, David Wagner described some of the more basic security flaws in Diebold, Sequouia and Hart machines, and then said that those were less harmful than the ones which could not be publicly disclosed! All three systems have very weak or no use of encryption and all three are vulnerable in different ways to malicious viral code. The review team focussed only on the security code and could not comment on other parts of the code e.g. vote counting. Obfuscation Session: Interesting talks on both software and hardware obfuscation. The obfuscation technique for software is too much like a hack; it is an example of what malware developers might do to avoid detection. The hardware obfuscation is a legitimate way to protect intellectual property using physical variation in fabricated circuits. Network Security and Privacy Session: The first talk showed that connection time is the bottleneck in cellular networks and thus vulnerable to denial of service attacks by using up the pool of connection IDs. The second talk discussed various possible attacks on dense urban w-ifi networks. The last talk was about data mining of anonymised network data by profiling data flows for different websites. Work In Progress Session: Some of the WIP talks discussed virtualisation. One talk described how to use virtual machines to isolate malware. Another talk showed how to use virtual machines to subvert software licenses, using a form of replay attack. Yet another talked about using VMs to detect kernel modifying rootkits.

Dagstuhl Seminar "Frontiers of e-Voting"

2007-08-09T10:00:00.000+01:00

A few weeks ago I participated in the Dagstuhl Seminar "Frontiers of e-Voting," organized by David Chaum, Miroslaw Kutylowski, Ron Rivest, and Peter Ryan.

I always enjoy my Dagstuhl visits, and this particular seminar was no exception. In fact, I found that the mix of people and personalities at this event quite refreshing, as it wasn't just a "castle" full of the same-old people who all know each other and agree. We witnessed cryptographers arguing with activist/computer scientists, political scientists drinking with theoreticians, and hacker/activists playing pool with PhD students of all ilks.

I have subscribed to several participant blogs as a result of these interactions, including those (co-)run by Michael Alvarez and Ian Brown. Already a couple of posts have caught my eye, and I'll comment upon them here in later posts.

I was asked to have a highly active role on the first day. In the morning I chaired the first session of the whole event. It focused on a summary of existing voting systems that have been constructed by attendees. The following systems were discussed: CIVS, Adder, Digishuff, Scantegrity/PunchScan, Pret a Voter, CyberVote, the Belgian Voting System, Hack-a-Vote, U.E. (used in Brazil), and KOA. Each person summarizing a system had to explain the principles of the system (i.e., why it was built), when it was created, if the project is still running, if/how the source/system are available, what license it is available under, what size and kind of team created the system and at what cost, how has the system been used in real elections, what balloting systems/style are supported (FPTP = first past the post, STV = single-transferable vote, etc.), what programming language(s) and operating system(s) were used, how scalable the system is thought to be, and what lessons were learned. I was struck by how many systems were "open source", but how few speakers actually knew if the source was really available, what license was used, and how the system was designed and built. Such does not bode well as hints of software system quality. I, of course, asked every person also how the system was specified and checked for "correctness". Where requirements gathered and analyzed? Was the system and architecture designed? Were assertions used in some way? How was the system tested? In general, the answer was always either "we make no claims that this system implements anything" or "the correctness of the software system is completely unimportant". The first of these claims is the honest one. The design and implementation of these experimental systems, without fail, have been haphazard, at best. Even one of my favorite systems, CIVS, which is implemented in a research programming language called JIF (Java + Information Flow), and uses very advanced distributed systems and cryptography constructs, contains little docs and no assertions according to one of its authors. The latter claim comes from the e-voting sub-community that focuses on end-to-end schemes. End-to-end voting systems are meant to provide very strong guarantees about a given elections integrity and voter privacy, typically by virtue of very smart algorithm design (and that's not just computational algorithms, but these systems involve people, organizations, physical artifacts like ballots, etc.) coupled with interesting cryptography. The mantra of this group is "verify the election, not the software". Unfortunately, nearly universally these system do use hardware and software to print and scan ballots, sometimes collect a voter's choices, transmit ballots, perform vote tallies, and report results. When something goes wrong, in essence, the crypto catches it, but where is the fault? At the moment, no one really knows how this auditability and culpability-management work. Furthermore, if the software and hardware is of poor quality, then the fault is likely to be found there in these relatively complex systems. So, while the mantra is "verify the election, not the software", what is actually meant is "verify the election and make sure the software is of high quality, don't just verify the software then trust the election"...a sentiment with which I completely agree.

End-of-Year Update on ESC/Java2

2006-12-17T11:30:00.000Z

One of the tools that we work hard on here at UCD is ESC/Java2. This post is to provide an end-of-year update on this popular tool. First, I plan on working on the first version of the ESC/Java2 User's Guide during the holiday break. Mikolas Janota and Radu Grigore, two of my PhD students, are continuing to work on their new specification-aware dead-code/assertion identification subsystem. We'll be writing a paper about this next quarter. Many people outside of UCD contribute to ESC/Java2 as well. We are excited to see collaborators Patrice Chalin and Perry James's work on the IDC subsystem continue to come in. We look forward to trying it out! My PhD student Alan Morkan is very unfortunately leaving us for greener pastures, as he has decided that doing a PhD is not in the cards right now. He and I are in the middle of writing a paper on the specification consistency checker, and I am trying to inspire him to help finish up the first version of the soundness and completeness warning system, which has been on hold while he has figured out his future. If anyone else would like to help finish up that subsystem, please drop me a line. I hope to have PhD student Michal Moskal visiting next semester for some time to work on ESC/Java2's prover backend and his theorem prover. We are very much looking forward to having him around for a few months. I have also been working with Clark Barrett CVC3 (the upcoming new version of CVC Lite) again lately, helping ensure it builds and runs well on OS X. Consequently, we hope to see the CVC3 and SMT-LIB backends move forward again next quarter. We are expecting some commits from MSc graduate Ke Sun in Eindhoven (supervised by Kuiper and Huizing and advised by Erik Poll). He has improved the PVS backend considerably and has some patches to the logic and the code as a result. His work is detailed in his thesis entitled "Verifying Java Programs by Integrating ESC/Java2 and PVS." Finally, I would like to put out a new beta release for the New Year, right after I have a first draft of the User's Guide. Coincident with this release will be a public announcement of the new version of the ESC/Java2 plugin that Aleksy Schubert has helped out with. I want to express my gratitude to all ESC/Java2 contributors and collaborators. Without you all this effort simply would not succeed. Happy holidays all. --Joe

ESF Workshop on Challenges in Java Program Verification

2006-11-18T13:41:00.001Z

From Monday to Wednesday, the 16-18 of October 2006, I participated in the European Science Foundation's workshop on "Challenges in Java Program Verification." This workshop was graciously organized by Reiner Hähnle from Chalmers University of Technology and Wojciech Mostowski from Radboud University Nijmegen. This workshop invited around twenty researchers working in Java program verification to come to Nijmegen, NL and give talk about recent work and, more importantly, talk with each other about our successes and failures as individuals and as a field, discuss where we should head next (again, collectively and individually), how we should organize ourselves, etc. I gave the opening talk on Tuesday at this workshop. My talk was called "Usable Formal Tools" and focused on the non-technical aspects of building a successful verification tool. On Wednesday afternoon I chaired a panel section called "Past Experiences and Lessons for the Future." The abstract for this panel was as follows:

Many of us actively took part in the development of a verification tool for OO languages. As in all research tools one has to make design and technology decisions that in the end may turn out to be suboptimal. Are there things that we can learn from each other? Which mistakes did we make in designing our verification tool? Which technologies worked and which didn't? Which lessons did we learn for the future?

Panel participants, and the tools with which they are associated, were:

Erik Poll on the Loop tool
Claude Marché on Krakatoa
Peter Müller on Jive
Joe Kiniry on ESC/Java2 (and a bit on Simplify and OBJ3)
Steffen Schlager on KeY
Mariela Pavlova on Jack
Kurt Stenzel on KIV
Rustan Leino on Boogie (and a bit on ESC/Java)
Robby on Bandera, Bogor, and Kiasan

I asked each panel member to discuss at most two positive and two negative (not necessarily unique) things that they learned from their tool experiences. I took notes of the responses of the panel members. But what I present here is my interpretation of a much longer statement, so any errors are my own and I apologize for any mis-interpretations. (Panel participants please feel free to write responses or clarifications to this blog post.) Peter Müller:

pros

use someone elses prover on the backend
use a small sound core logic (about 24 rules)

cons

working on a small language subset - use a real language instead
underestimated the amount of work that is necessary to build a tool

Erik Poll:

pros

it is feasible to define a semantics of a real language (e.g., Java)
reimplementation of a tool from scratch is sometimes necessary

cons

deep embeddings do not work well in practice
underestimate workload and keeping tool alive and usable

Rustan Leino:

pros

use an intermediate language
develop a rich test suite

cons

some aspects of the test suite are weak (completeness, coverage, evolution)
documentation, particularly no document describing logic

Claude Marché:

pros

using an intermediate language works well
support multiple provers (via the why tool)

cons

cooperating provers is very difficult or not possible
underestimate work involved in building a tool and have few developer

Mariela Pavlova:

pros

splitting tactics and having a rich UI
good intermediate representation

cons

underspecification of architecture, lack of documentation
problems in semantics that prevent certain VC possibilities

Robby:

pros

design early and modularly
bells & whistles for effective sales and use

cons

"quick and dirty" leads to dirty - aka don't overdesign
complex architecture and code

Kurt Stenzel:

pros

use an existing foundation
formal proof of properties of calculus and semantics

cons

good for complex interactive proofs, but bad for simple things
limited manpower (i.e., no JML support)

Steffan Schlager:

pros

symbolic execution is an excellent reasoning technique
JML support is crucial (i.e., use a "real world" language)

cons

using provers that use decision procedures does not provide any evidence
core data structures overly focused on Java

Joe Kiniry:

pros

community support via growing a community and giving good support
used real software engineering practices

cons

complexity of architecture and evolution, given history
using real software engineering practices

Several audience members also had some things to contribute as well. In particular, Arnd Poetzsch-Heffter argued that, given the number of groups working on tools, and the fact that none of them have sufficient resources to accomplish all of their goas, some common tool foundation seemed to be necessary. This is not a unique perspective. A handful of us in the verification community have argued for such over the past several years. Unfortunately, like many other communities in Computer Science, the verification community is full of researchers who have Not Invented Here syndrome when it comes to developing new tools. I find this amusing and frustrating, given how many researchers have no problem at all standing on the shoulders of theoretical giants, but refuse to even sidle up to the big toe of the practical. It is our intention that the Mobius Program Verification Environment, on which we will write more later, be exactly such a common foundation. The other point made by several tool builders is a positive emphasis on intermediate representations. There now have emerged several high-quality intermediate representations which we in the Mobius community are convinced are the proper foundations for inter-operable, maintainable, long-lasting tool suites. In particular, we would like to draw your attention to the following (non-exhaustive) list of excellent intermediate representations with tool and community support:

If we have missed essential intermediate representations, please point them out to us! -Joe Kiniry

Welcome to the AFM Blog

2006-11-06T23:49:00.000Z

Welcome to the Applied Formal Methods Blog, founded by the KindSoftware Research Group.

In this blog my friends and I will post about software engineering with applied formal methods.

As none of us are big bloggers, do not expect a ton of content.

But we hope that what we do write will, as a result, be interesting and useful to you, our readers.

Please contact us if there are particular topics in AFM you would like us to comment upon.

Or, if you are a user or researcher of AFM and are interested in contributing, drop us a line.

-Joe Kiniry