Eric Mercer

Discussion: sharing classes or becoming a center of excellence for formal verification:

• Use conference calls, VNC, and webcams to talk more amongst the various Universities
• Cross list classes between Universities: the easiest way to do this is to use independent study courses. Need to work out the accounting for keeping track of how many students are taking courses on and off campus.
• John: we should share software tools too. We can share our software infrastructure to help us progress as a group and compete with larger groups.
• Chris: meeting more regularly would help a lot. Meeting to talk more in depth about research topics would help too.
• Scott: I would be more inclined to use a research tool (not my own) if I know the developer was nearby to help me make the tool useful.
• Mike: we seem to implementing the same ideas all over again. Key point, none of us are good an everything. We can use strengths of other researchers
• RU Sites deadline is coming up in August.
• We have many classes coming in the fall. Many different courses being taught in all Universities.
• Action items: need to get the VNC working on all three campuses.
• Biweekly seminar where we only do one talk. Use skype or just originate call from University that can afford long distance call.
• Long term goal: get center of excellence (IGERT or Science and Technology center of excellentce). Need to talk to Dean's and help them understand what we are trying to do.
• Distance learning is a fundamental cultural change.
• Need someone in each university to talk to upper level of administration to talk about our ideas and needs.
• RU grant is a lot of work. Need to bring in students from outside of University. Need to provide an entertaining camp. Must be really professional. Really sacrifices an entire summer.
• Need a list of classes being taught in each University for all semester. Need to work how how to get our students ability to enroll in off campus classes and get credit.
• IGERT is a much more appealing money source for this.
• Need a mailing list (Mike Jones).
• Web stuff.
• Berkeley website for shared tools etc. as template. Need someone to host all of our tools with all the course information (Pryank Kalla).
• Can webcam and stream courses if needed for courses that are not slide based.
• Sharing courses helps facilitate sharing course materials. Possibly standardize courses and make it possible to offer them each semester with the different universities hosting the course each semester

These are a few of my notes from the various presentations. I had to come in and out quite a bit, unfortunately, so I missed some of the presentations.

• Neha Rungta (Guided Search): no significant questions. John Reghr had a nice summary which is, "The context in the run time stack prunes out many infeasible paths."
• Rahul Kumar (Paged hash tables):
  • It seems like this hash table readily lends itself to a form of disk based model checking. It would be very easy to move pages off to disk and only keep resident in memory pages that are active. We could easily implement an algorithm for caching pages in memory base on usage history rather than actually load-balancing across computation nodes nodes.
  • What type of algorithms should be used to actually balance the table.
  • Hash table load balances space, but does have effect on computation as well. Need to investigate how moving space affects space.
• Pryank Kalla (RTI Verification): I had to step on the first presentation to make lunch reservations.
  • the canonical representation of the polynomial results in a better synthesized data path than the noncanonical form. Very interesting. I wonder how this could be used to improve synthesis.
• Pryank (CNF SAT Search):
  • Time is a real problem in SAT solver.
  • Had to step out again. Not having any luck today.
  • Work looks very interesting.
  • Mike Jones: if you do it with 10^6 variables, how big do you graphs get? They do not build the graphs directly. It is all implicit. They only have a modest increase in space.
  • What is the complexity? It is square or cubic in the number of nodes (variables). It is actually v^2c.
• Ganesh, University of Utah: Students are working in a lot of interesting places. Ganesh mentioned that verifying adders is a big deal right now. Also, industry is not interested in a complete verification. Bugs found are their metric. Muprhi is still useful for cache protocol verification. Working on a partial order reduction for murphi. Working on symbolic stuff in partial order reduction. Converts everything to a Boolean expression and sends it to a SAT solver. The SAT solver checks to see if two transitions are independent. The independent check takes time. Key to computing the ample set in the SAT algorithm. Symbolic methods do not seems to work for cache coherency verificaiton. Ganesh is working on a mu2smv translator. Use this translator to execute a few steps on enabled transitions and then send the resulting states to a SAT solver to check of independence in the ample set computation. Igor Melatti possible coming to University of Utah. Would be very nice to visit with him on his disk cache work.
  • Distributed model checking: network calibration to find optimal packet sizes. Has 2 softMC papers www.cs.utah.edu/formal_verification. These are SPIN papers. Refactored SPIN for parallel execution using the network analysis tool. A nice graph visualization tool is Guess. Works on graphs that cause GraphViz to kill over and die.
  • Trying to verify hierarchical cache coherence protocols.
  • Generating the SAT problem is what is incurring big run times. Not solving the SAT problem.
  • Ganesh is only testing load/store sequences on the coherence test. Not arithmetic stuff. Trying to see if chip implements Itanium coherence rules.
  • Verifies load bypasses etc. as specified in documents.
  • Other work is to verify large scale MPI programs for scientific computing (Gauss).
  • Zing is Microsoft's model checker. Has a very clean input language. Would love to get a copy of this.
  • Cool papers: Pasareanu, Pelanek and Visser's new paper on abstract matching refinement; Prasad's survey of advances in SAT based verification. Patrick Cousot's notes on abstract interpretation at MIT.
• John Reghr (University of Utah)
  • Analyzing object code: stack depth and worst-case execution time
  • Analyzing source code: C-code for limited range detection, memory alias analysis, interrupt handlers, threads, etc.
  • Combine object code and source code analysis: src ---> compiler ---> object use both in analysis to create transformations on the course code to feed back into the compilation process.
  • Compiler optimization for resource constraints: how to compiler code to meet needs in a resource constrained environment.
  • Need better analysis infrastructure. This is what Nathan Cooprider is going to present.
  • TinyOS written in NesC (Source to source translator NexC to C.
  • CIL (UCB) translates C programs into a canonical form with single loop construct and syntactic sugar removed. Can process Linux Kernel.
  • Nathan's framework sounds really cool. Has all infrastructure for abstract interpretation and program transformations based on abstract states. Very nice.
  • Seems like the Framework would support nicely a model checker built on top of it with abstract interpretation similar to the Visser work in CAV 2005. Very interesting.
  • Abstract interpretation is very interval based. Fits nicely for domain abstraction.
  • Must define abstract interpretation of operations (add, OR, etc.) on these interval domains.
  • Tool lets you define the abstract computation of various operators for any architecture. Make abstract interpretation very easy.
  • Only need to specify concrete operators, and the tool lifts the concrete operator into the abstract domain if the operator fits, for example, ripple-carry structure etc.
  • Tool supports bit-wise and interval domains currently.
  • It would be interesting to better understand the difference between symbolic execution in trajectory evaluation and abstract interpretation.
• Annette Bunker (Utah State University)
  • Vision is to make Model Checking accessible to design engineers.
  • Live sequence charts (PLSC) for protocol verification
  • Cold conditions are optional assertions
  Hot conditions are required assertions
  • Charts support regular expressions around groups of transactions in the protocol.
  • Horizontal bars indicate passage of times or clock edges.
  • PCI, wishbone, VCI, advanced extensible interface, and Itanium have been tackled. AEI and Itanium are pipelined protocols.
  • Cold conditions are used for loop conditions.
  • Live sequence charts might help in the verification class to teach LTL an CTL. Students can create charts from protocol spec and then write LTL properties.
  • Wishbone may be small enough. May be even PCI. The idea is that a student can implement a protocol in BIR using threads etc. and then we can write specification for the protocol to verify through the remainder of the class.
  • For STE, only outgoing events are used in the consequences. Incoming edges are for the antecedent. Antecedent (A) and cedent (C) form an implication A --> C
• Chris Myers, University of Utah, Analogue Circuit Verification
  • Analogue circuits are everywhere, and there are not a lot of tools to verify analogue circuits; especially in the context of digital circuits.
  • SPICE is a deterministic model. Answers are always the same. Most testing is somewhat ad hoc or random looking for possible defects.
  • Simple example: integrator circuit. Does the integrator ever hit saturation?
  • Circuit does saturate, but it is not obvious how to get SPICE to show the saturation---SPICE can find it, but it is largely due to rounding errors resulting from long SPICE simulations the simulate many cycles of the circuit.
  • Abstract interpretation domain has octagon and polyhedra domains that directly correlate to the zone representation using linear inequalities. The polyhedra are more verbose and can represent arbitrary polyhedra that are not restricted to just x - y < c --- no coefficients on the variables.
  • There is a lot of conservative approximation in the state space to accommodate the zone representation. The assumption is that the precision sacrifice is worth the gain in speed and ability to actually complete.
  • False positives are a real problem because of the conservative approximation.
  • Modeling differential equations: break into constant regions of rate.
  • Symbolic verification of the hybred Petri-nets is very cool. The computation of the preimage in the time representation is very hard and complicated. Must introduce the new variables to represent the new zones that can exist in the preimage.
  • Classical control works well for linear systems, but many systems are nonlinear, and need this new type of analysis.
  • Can you solve this problem using ILP? Unroll and do a bounded approach.
• Konrad Slind, University of Utah, HOL
  • Cryptol is a language for cryptographic systems
  • Working on a refinement system that takes high-level description and refines it to hardware. Prooves every step of the refinement. It is all automated.
  • Krakatoa --- verifier for Java examples.
  • Teaching HOL and theorem proving: project class; getting students up and running was really hard. 75% of the time was spent trying to get students up to speed as competent tool users in theorem provers.
  • Need to help students learn what to do when they get stuck. This is part of interactive theorem proving. What do you do when you get stuck?
  • Most successful projects started from existing formulations.
• Mike Jones, Brigham Young University: brief overview and a few thoughts on teaching formal methods.