Galois is excited to announce the Open-Source release of FiveUI! FiveUI is a framework and tool for checking web-based user interfaces against codified UI guidelines. It is the first step towards an extensible, semantically aware, reusable and pragmatic toolchain for checking aspects of user interfaces against arbitrary guidelines. FiveUI currently works as a browser extension […]

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.

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.

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: […]

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 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 […]

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 Wednesday, 11 January 2012 title: Model-based Code Generation and Debugging of Concurrent Programs speaker: Borzoo Bonakdarpour […]

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.) title: Formalizing Haskell 98 in the K Semantic Framework speaker: David Lazar time: Tuesday, 10 January 2012, 10:30am location: Galois Inc. 421 SW 6th Ave. Suite 300, […]

We are pleased to announced the availability of a new tech talk video, Eric Migicovsky talking about his experiences with a hardware startup. More details about the talk are available at the talk announcement page. For more Galois tech talk videos, please visit our Vimeo channel.

HTML5 is coming, and it’s not just the next version of HTML.

HTML began as a lightweight mark-up language for linking documents on the web, with some rendering hints. As new versions have come along, support has been added for new kinds of content (images, video, interactive content). More recently, interest has grown in understanding documents and web applications on a deeper level. The most prominent example of this is the semantic web, which seeks to move from a “web of documents” to a “web of information”.

All previous versions of HTML make this an extremely challenging task, akin to trying to understand a philosophical text presented in terms of its typography.

HTML5 will change that. The designers of HTML5 have taken great care to separate semantic content (the information a document is intended to convey or represent) from the process of rendering (how a document should appear in a browser). Through this “separation of concerns”, HTML5 is equipped to revolutionize how we think of the web, how we work with it, and how we create new content. Our interest is in the potential for HTML5 to change how we specify, design, build, and analyze user interfaces – wherever they may appear: on the web, mobile devices, or desktop.

With consistent user experience as our guiding motivation, we survey the state of the art and practice of tool support for semantic reasoning about HTML5.