Since the early days of computing, Bell Labs researchers have contributed in significant ways to the development of software engineering.
Doug McIlroy created one of the earliest unification algorithms. Two of the best known program verification tools, SPIN (initiated by Gerard Holzmann) and COSPAN (initiated by Bob Kurshan) were developed at Bell Labs. Others researchers have advanced the theory and algorithms for automated reasoning, such as the development of timed automata, partial order reasoning, automated program abstraction, abstraction refinement and directed program testing.
Today, software engineering research is an integral part of several activities under way in Nokia Bell Labs, particularly so in those that incorporate highly distributed and/or virtualized elements. Kedar Namjoshi, Dennis Dams and Ramesh Viswanathan are exploring notations and algorithms for the formal analysis of concurrent and distributed software. Topics include the design of new static analysis algorithms, and compositional reasoning and symmetry reduction methods. The goal is to tackle state explosion, which arises in concurrent system analysis, and then to produce parametric proofs of correctness which are then applied to arbitrarily large configurations. The solution relies on comparison of local symmetries between node neighborhoods, and this reduces the proof obligation to one over a single representative node.
Tackling state explosion in software with compositional verification and localized symmetry
Large-scale data analysis in cloud-based environments is another area of active software engineering research. Alan Jeffrey’s work on the basic principles for structuring and analyzing functional reactive programs has application to the design of large data-stream analysis networks. Pete Fales is investigating the design and the performance of NoSQL databases in environments where guarantees on tail latencies in request-response protocols are needed.
Other research activities are focused on access control and the investigation of links between program verification and compiling. In the former, Glenn Bruns is working on access control formulations that allow hierarchical composition of policies. An example of the latter is Kedar Namjoshi’s research on self-certifying compilers capable of generating checkable proofs of their own correctness.