Eric Mercer

May 25, 2005

Notes and throughts URVW 2005

We had 26 people attend from 3 different universities. We covered a wide range of research, and I thoroughly enjoyed the conference. There is a lot of interesting work being done in Utah. These notes are just a few random thoughts, and a brief summary of our discussions. I think the bottom line is that we have a great potential to work together and build a strong research and education program for verification and analysis here in Utah. Thanks to everyone who helped to make this a great workshop.

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.

Posted by egm at 09:32 AM | Comments (0)

May 16, 2005

The 2nd Annual Utah Regional Verification Workshop on May 25, 2005

The Computer Science Department at Brigham Young University is pleased to host the second annual Utah Regional Verification Workshop (URVW). The workshop is a forum for Utah researches to share their current work in verification and validation; and it is a chance to bring the community together to foster discussion and possible collaborative projects between the various Universities in Utah. Currently, we have folks coming from the University of Utah, Utah State University, and BYU. The workshop is open to anyone; although, if you want to be on the program, then you need to email Mike Jones (jones at cs byu edu) as soon as possible since the schedule is mostly finalized at this point.

The actual workshop will take place in room 136 of theTalmage Math Sciences/Compute Building (TMCB). This is building number 79 on the PDF version of the campus map. For your confusion, it is building number 80 on the online interactive campus map. Room 136 is on the main floor on the east side of the building (i.e., the part of the building that is nearest the mountains and farthest from Utah lake for those who are directionally challenged). Room 136 is a technology enhanced classroom which means it has a PC connected to a projector (1024x768 resolution) with appropriate cables and software to connect it directly to your laptop or flash drive. The PC itself is a network enabled Windows XP box with Adobe Reader and PowerPoint installed. Please email myself (egm at cs byu edu) or Mike Jones (jones at cs byu edu) if you have special equipment needs for your presentation.

For experienced BYU users, you can skip the following directions: getting to BYU is usually a fairly easy thing to do, and detailed directions are included with the PDF version of the campus map. If you are traveling South on I-15, then you will want to take the University Parkway Exit just after the Orem Center Street exit. Go east on University Parkway (toward the mountains and away from the lake) and eventually you will see the football stadium. Continue east through the light at the football stadium to 450 East at the light in front of the Marriott Center, and turn right. Go south on 450 east until you reach the next light, which is at North Campus Drive, and turn left to go east. There are two different visitor parking lots at BYU. The first is just off of North Campus Drive as you approach the museum; this is building 63 on the PDF version of the campus map. This parking lot is closest to TCMB. North Campus Drives curves around to the south and becomes East Campus Drive. The next visitor lot is just off of East Campus drive across from building 92 on the PDF version of the campus map. Both visitor lots are free

The current schedule for the workshop is as follows:

09:30 AM	Eric Mercer, Brigham Young University, Improving Error Discovery using Guided Search and A Paged Hashtable for Distributed Model Checking
10:00 AM	Priyank Kalla, University of Utah, RTL Verification of Polynomial Datapaths and Variable Ordering to Guide CNF-SAT Search
10:30 AM	Ganesh Gopalakrishnan, University of Utah, Gauss: A Framework for Verifying Scientific Computing Software
11:10 AM	John Reghr, University of Utah, Generating Abstract Transfer Functions and Leveraging CIL to provide a static analysis framework for embedded systems written in C
11:50 AM	Annette Bunker, Utah State University, Hardware Protocol Verification Using Protocol Live Sequence Charts
12:20 PM	Lunch
01:50 PM	Chris Myers, University of Utah, Formal Verification of Analog and Mixed-Signal Circuits
02:30 PM	Konrad Slind
03:00 PM	Break
03:15 PM	Mike Jones
03:45 PM	How can we better coordinate and collaborate?
04:45 PM	Target ending time

We will provide refreshments for each of the breaks, and there will be a light breakfast (i.e., muffins and juice) for the morning. Please be aware that in accordance with the values and standards of BYU, no alcohol, tobacco or caffeinated products are to be brought onto the campus. We have not settled on a lunch location yet, but we expect the cost to be around $10 per person. More than likely, however, we will eat in either the Skyroom Restaurant or the new Legends Grill. Check back for more details.

Posted by egm at 01:59 PM | Comments (0)