HTML5 is Paving the Way for Semantically Aware Tools

Rich semantics are the Holy Grail for automated analysis tools; combined with extensible, familiar, and reusable tools and techniques we can seriously cut the costs associated with robust user interface development and testing.

Previously, we discussed the set of tools available for validating and linting HTML5-based user interfaces; (eg: the  W3C, numerous HTML/CSS editors, and tools like  HTML Lint). These tools help to identify syntactic issues, but what else is possible? The syntactic (and limited semantic) checks that these tools perform are necessary, but they aren't sufficient to cover the body of intricate failures that can occur while creating the rich user experiences we've come to expect from interactive web applications and mobile devices. Linters and Validators can't, for example, find bugs relating to the visual layout, and with good reason: Checking a UI is hard; it's repetitive, monotonous, and more importantly, subjective work.

However, there is still room for improvement. Surely we can push the envelope to do more. What's next, and how can we automate tasks that still challenge human analysts?

The first important insight is that many general guidelines for creating a good user interface have quantitative approximations. For example, the Windows 7 guidelines state:

Use title-style capitalization for titles, and sentence-style capitalization for all other UI elements.

and:

Write the label as a phrase or an imperative sentence, and use no ending punctuation.

In the words of Richard Anderson: We have the technology! Which brings us to the first of a few key areas or techniques that could improve the tools that help ensure UI Consistency.

Click to read more ...

Tech talk video: Efficient Implementation of Property Directed Reachability

We are pleased to announced the availability of a new tech talk video, Alan Mishchenko talking about an efficient implementation of a novel model checking technique. For more information, please visit the talk announcement page.

For more Galois tech talk videos, please visit our Vimeo channel.

Tech Talk: Efficient Implementation of Property Directed Reachability

Galois is pleased to host the following tech talk. These talks are open to the interested public--please join us! (There is no need to pre-register for the talk.)

Please note the unusual date and time for this talk, it is on Monday, 6 February 2012, at 10am.

title: Efficient Implementation of Property Directed Reachability

speaker: Alan Mishchenko

time: Monday, 6 February 2012, 10:00am

location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract:

Last spring, in March 2010, Aaron Bradley published the first truly new bit-level symbolic model checking algorithm since Ken McMillan’s interpolation based model checking procedure introduced in 2003. Our experience with the algorithm suggests that it is stronger than interpolation on industrial problems, and that it is an important algorithm to study further. In this paper, we present a simplified and faster implementation of Bradley’s procedure, and discuss our successful and unsuccessful attempts to improve it.

Relevant links: the paper, slides for the talk.

bio: Alan Mishchenko graduated from Moscow Institute of Physics and Technology, Moscow, Russia, in 1993, and received his Ph.D. degree from Glushkov Institute of Cybernetics, Kiev, Ukraine, in 1997. He has been a research scientist in the US since 1998. Currently, Alan is an Associate Researcher at University of California, Berkeley. His research interests are in developing computationally efficient methods for logic synthesis and verification.

New tech talk video: Formalizing Haskell 98 in the K semantic framework

We are pleased to announced the availability of a new tech talk video, David Lazar talking about formalizing Haskell 98 in the K semantic framework. For more information, please visit the talk announcement page For more Galois tech talk videos, please visit our Vimeo channel.

Galois Tech Talk (3/3 next week!): On deadlock verification in micro-architectural models of communication fabrics.

Galois is pleased to host the following tech talk. These talks are open to the interested public--please join us! (There is no need to pre-register for the talk.)

Please note the unusual time for this talk, it is on Thursday, 12 January 2012

title: On deadlock verification in micro-architectural models of communication fabrics.

speaker: Julien Schmaltz

time: Thursday, 12 January 2012, 10:30am

location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract:

Communication fabrics constitute an important challenge for the design and verification of multicore architectures. To enable their formal analysis, micro-architectural models have been proposed as an efficient abstraction capturing the high-level structure of designs. Micro-architectural models also include a representation of the protocols using the communication fabrics. This combination of different aspects in a single model is crucial for deadlock verification. Deadlocks emerge or are prevented in this combination: a system with a deadlock-free communication network combined with a deadlock-free protocol may have deadlocks or a system with a network with deadlocks combined with a deadlock-free protocol may be deadlock-free. This combination also makes the verification problem more complicated. We will present an algorithm for efficient deadlock verification in micro-architectural models. We will discuss the limitations of this approach and point to future research direction. An important future application of our methodology is the verification of cache coherency at the level of micro-architectures.

bio: Dr. Schmaltz is assistant professor at the Open University of the Netherlands. He is also affiliated with the Digital Security group at the Radboud University Nijmegen. He obtained a PhD from the University of Grenoble in 2006. Before joining the Open University he was a postdoctoral researcher at the University of Saarland (Germany), the Radboud University Nijmegen, and the Embedded System Institute in Eindhoven (The Netherlands). During his PhD, he visited the University of Texas at Austin. His research currently focuses on the use of formal methods in the verification of on-chip communication architectures. His general research interests include the application of formal methods in security, certification, software engineering, hardware design, and model-based testing. He co-authored more than 40 publications. In 2011, he co-chaired the second international conference on Interactive Theorem Proving and the 10th edition of the international workshop on the ACL2 Theorem Prover and its Applications.