My first stop of the day was to sit in on session 4.2 - High Level Validation Models. A few things caught my attention at this session. First, and reminiscent of my experience last year at DATE was a comment made by the third presenter, Joao Marques-Silva from Southampton University in the UK. The title of Joao's presentation was "Algorithms for Maximum Satisfiability Using Unsatisfiable Cores." During his opening remarks, Joao mentioned that knowledge of SAT solvers was required to understand his presentation. He continued: "If you don't understand SAT, tough!" Eh? Many of the talks last year had this type of strong academic bent. I believe many of the session attendees did understand SAT, but for those of us who didn't the discussion that followed was absolutely meaningless.