Almost all software contains defects. Some defects are found easily while others are never found, typically because they emerge seldom or not at all. Some defects that emerge relatively often even go unnoticed simply because they are not perceived as errors or are not suffciently severe. Software defects may give rise to several types of errors, ranging from logical/functional ones (the program sometimes computes incorrect values) to runtime errors (the program typically crashes), or resource leaks (performance of the program degrades possibly until the program freezes or crashes). Programs may also contain subtle security vulnerabilities that can be exploited by malicious attackers to gain control over computers.    Fixing defects that suddenly emerge can be extremely costly in particular if found at the end of the development cycle, or worse: after deployment. Many simple defects in modern programming languages can be found by modern compilers, e.g. in statically typed languages. But the predominating method for finding defects is testing. Testing has the potential of finding most types of defects, however, testing is costly and no amount of testing will find all defects. Testing is also problematic because it can be applied only to executable code, i.e. rather late in the development process. Alternatives to testing, such as data°ow analysis and formal verification, have been known since the 1970s but have not gained widespread acceptance outside academia|that is, until recently; lately several commercial tools for detecting runtime error conditions at compile time have emerged. The tools build on static analysis and can be used to find runtime errors as well as resource leaks and even some security vulnerabilities statically, i.e. without executing the code. This paper is a survey and comparison of three market leading static analysis tools: PolySpace Verifier, Coverity Prevent and Klocwork K7. The list is by no means exhaustive, and the list of competitors is steadily increasing, but the three tools represent state-of-the-art in the field at the moment.

The main objective of this study is (1) to identify significant static analysis functionality provided by the tools, but not addressed in a normal compiler, and (2) to survey the underlying supporting technology. The goal is not to provide a ranking of the tools; nor is it to provide a comprehensive survey of all functionality provided by the tools. Providing such a ranking is problematic for at least two reasons: Static analysis is generally only part of the functionality provided by the tool; for instance, Klocwork K7 supports both refactoring and software metrics which are not supported by the two other tools. Even if restricting attention only to static analysis functionality the tools provide largely non-overlapping functionality. Secondly, even when the tools seemingly provide the same functionality (e.g. detection of dereferencing of null pointers) their solutions are often not comparable; each tool typically finds defects which are not found by any of the other tools.

Studying the internals of commercial and proprietary tools is not without problems|in particular, it is impossible to get full information about technical solutions. However, some technical information is publicly available in manuals and white papers; some of the tools also originate from academic tools which have been extensively described in research journals and conference proceedings. While technical solutions may have changed since then, we believe that such information is still largely valid. We have also consulted representatives from all three providers with the purpose to validate our descriptions of the tools. Still it must be pointed out that the descriptions of suggested technical solutions is subject to a certain amount of guessing in some respects.

The rest of the report is organized as follows: In Section 2 we define what we mean by the term static analysis and survey some elementary concepts and preconditions; in particular, the trade off between precision and analysis time. Section 3 contains a description of basic principles of static analysis. In Sections 4{6 we survey the static analysis functionality provided by PolySpace Verifier/Desktop, Coverity Prevent and Klocwork K7 focusing in particular on the support for the C and C++ programming languages. Section 7 addresses the complementary issue of programming guidelines such as those of The Motor Software Reliability Association (MISRA). Section 8 contains a qualitative comparison of the three tools summing up their relative merits and shortcomings. The section also surveys several industrial evaluations of the tools over time at Ericsson, in particular involving the products from Coverity and Klocwork. Section 9 contains conclusions.

We present a model based approach to diagnosability analysis for interacting ¯nitestate systems where fault isolation is deferred until the system comes to a stand-still. Local abstractions of the system model are used to alleviate the state spaceexplosion. Pairs of closely coupled automata are merged and replaced by a sin-gle automaton with an equivalently behavior as seen from the rest of the system;interaction between the merged automata is internalized and the new equivalentautomaton is subsequently abstracted from internal behavior irrelevant to fault iso-lation. In moderately concurrent systems these steps can often be iterated until thesystem consists of a single automaton providing a compact encoding of all possiblefault scenarios of the original model. We illustrate how the resulting abstractioncan be used as a basis for post mortem diagnosability analysis.

I maj 2004 genomfördes en enkätundersökning som riktades till alla doktorander vid Linköpings universitet. De frågeområden som enkäten behandlade inkluderade doktorandens bakgrund och nuvarande status; handledningssituationen samt forsknings- och arbetsmiljö; upplevd särbehandling; forskarutbildningskurser och seminarier; pedagogisk utveckling och undervisning, samt ett antal frågor om hur doktoranden såg på sin forskarutbildning, sin egen insats och på framtiden. Dessutom fanns möjlighet att i fritext ange vad som var positivt respektive negativt med utbildningen, samt att ge förslag på vad som borde förändras och bevaras.

Enkäten sändes till de cirka 1 360 personer vars e-postadresser var tillgängliga. Närmare 70 %, eller över 900 personer, svarade på enkäten; i ungefär samma omfattning på samtliga fakulteter. Ungefär 5 % uppgav inte någon fakultetstillhörighet. Cirka 45 % av de svarande angav att de var kvinnor, medan 52 % angav att de var män. Det var dock stora variationer i könsfördelningen på fakultetsnivå. Kvinnornas medianålder var något högre än männens, och åldersspridningen var störst på Hälsouniversitetet (HU). Doktoranderna vid Linköpings tekniska högskola (LiTH) var i genomsnitt yngst och en mindre andel av dem, jämfört med övriga, hade hemmavarande barn. Det var en högre andel kvinnor än män som hade hemmavarande barn. Ungefär tre av fyra bodde i Norrköping eller Linköping; en högre andel på LiTH, och en lägre andel på Filosofisk fakultet (Fil fak) och Utbildningsvetenskap (UV).

Drygt hälften av alla som svarade på frågan hade genomfört hälften eller mindre av sin forskarutbildning. Att vara antagen till licentiatexamen var betydligt vanligare på LiTH (ca 12 %) än på övriga fakulteter. Drygt en fjärdedel av de svarande deltog i någon forskarskola. Det vanligast skälet till att ha gjort ett längre uppehåll var föräldraledighet (8 %) följt av förvärvsarbete (5 %).

Den vanligaste formen av försörjning var doktorandanställning, men det fanns stora skillnader mellan fakulteterna/motsvarande. HU hade lägst andel. En tredjedel av doktoranderna där hade istället klinisk tjänst. Drygt 80 % av de forskarstuderande vid LiTH hade doktorandanställning. Att enbart ha utbildningsbidrag var sällsynt på samtliga fakulteter, medan kombinationen utbildningsbidrag och assistenttjänst förekom; och då mest frekvent vid HU (drygt 12 %). Den vanligaste uppgivna aktivitetsgraden oavsett fakultet var mellan 90 och 100 % (cirka 25 % av de svarande) medan det på HU fanns en andel – nära 20 % – med mycket låg aktivitetsgrad (0–10 %).

Doktoranderna var tämligen nöjda med sin utbildning. På en femgradig skala där 5 stod för ”mycket bra” och 1 ”mycket dålig” hamnade medelbetyget på forskarutbildningen på 3,65. Doktoranderna på Filosofisk fakultet och LiTH satte ett något högre betyg, men variationerna mellan fakulteterna var små. Betyget på den egna insatsen sattes av de allra flesta något lägre, medelvärdet var 3,60 på samma skala. De mer detaljerade frågorna om handledning och avhandlingsarbete hade i flera fall högre medelvärde: Handledarens intresse för doktorandens forskning, handledarens läsning av texter, förekomsten av konstruktiv kritik och doktorandens förtroende för handledaren låg nära värdet 4 på den femgradiga skalan. Lägre medelvärden gavs på frågan om handledaren underlättar för doktoranden att få kontakt med andra forskare. Tiden som användes för handledning skiftade en del mellan fakulteterna, men sammanfattningsvis fick cirka 80 % av alla doktorander 1–10 timmar handledning per månad. Filosofisk fakultet och Utbildningsvetenskap hamnade oftare i den nedre delen av intervallet och LiTH samt HU i den högre delen. Uppfattningen att tiden som gavs svarade mot behovet skiftade. Mest nöjda med tidens omfattning var doktoranderna på Utbildningsvetenskap; minst nöjd var man på LiTH.

På frågorna om forskarutbildningskurser hamnade medelvärdena lägre än på frågorna om handledning. Det var liten skillnad mellan forskarskoledoktorander och övriga på dessa frågor.

Rent allmänt var alla mycket nöjda med sin forsknings- och arbetsmiljö. Genomgående fick frågorna inom det området högt medelbetyg, med undantag för dem som rörde tillgången till nationella och framför allt internationella forskarnätverk. Den sociala miljön i doktorandgruppen skattades högre än densamma på institutionen i sin helhet.

Enkäten innehöll även frågor om upplevd positiv och negativ särbehandling. Cirka 50 personer, med få undantag kvinnor, instämde i att de upplevt negativ särbehandling på grund av kön (svarade 4 eller 5 på den femgradiga skalan). Ingen fakultet utmärkte sig i detta avseende.

Institutioner med en jämn könsfördelning föreföll ha färre fall av upplevd negativ särbehandling. De som upplevt negativ särbehandling på grund av etnisk bakgrund, sexuell läggning eller social bakgrund var färre till antalet. Även positiv särbehandling hade upplevts – antalet svar var av samma storleksordning som för negativ särbehandling. Spridningen över fakulteter och institutioner var även här stor.

Efter disputationen kunde ungefär 70 % tänka sig en postdoc-period utomlands. Huvudskälet till att inte vilja åka var vanligen hänsyn till familjen, det vill säga situationen för barn och partner. Omkring hälften såg sina möjligheter som goda eller mycket goda att få ett arbete direkt efter examen.

Following the panel discussion at the International Conference on Logic Programming 2003 in Mumbai, India, the first international workshop on Teaching Logic Programming, TeachLP 2004, was held in Saint Malo, France, on 8–9 September 2004. The meeting ran as a workshop in conjunction with the 2004 International Conference on Logic Programming, held on September 6–10, 2004.

Logic Programming (LP) and Constraint Logic Programming (CLP) are powerful programming paradigms, but hard to learn without sufficient assistance. To further spread the technology it should be taught to a broader range of computer science students. The aim of the workshop was to investigate what is currently taught and how; what should be taught and why.

We propose a method for fault isolation in discrete event systems such as object oriented control systems, where the observations are the logged error messages. The method is based on automatic abstraction that preserves only the behavior relevant to fault isolation. In this way we avoid the state space explosion, and a model checker can be used to reason about the temporal properties of the system. The result is a fault isolation table that maps possible error logs to isolated faults, and fault isolation thus reduces to table lookup. The fault isolation table can also be used as an analysis tool at the design level to find both faults that cannot be isolated as well as redundant error messages.

We propose a fault isolation scheme based on model-checking in order to reason about temporal properties of loosely coupled systems of concurrent processes. To address the problem of state space explosion we advocate an automatic abstraction technique based on a notion of observational equivalence. We statically analyze a system and construct a total function from possible message logs to isolated faults. Thus, fault isolation reduces to table lookup. Tables can be used at design time to find non-diagnosable failures of the system as well as redundant error messages.

We propose a fault isolation scheme based on model checking in order to reason about temporal properties of loosely coupled systems of concurrent processes. To address the problem of state space explosion we advocate an automatic abstraction technique based on a notion of observational equivalence. We statically analyze a system and construct a total function from possible message logs to isolated faults. Thus, fault isolation reduces to table lookup. Tables can be used at design time to find non-diagnosable failures of the system as well as redundant error messages.

We present a logic programming based asynchronous multi-agent system in which agents can communicate with one another, update themselves and each other, abduce hypotheses to explain observations, and use them to generate actions. The knowledge base of the agents is comprised of generalized logic programs, integrity constraints, active rules, and of abducibles. We characterize the interaction among agents via an asynchronous transition rule system, and provide a stable models based semantics. An example is developed to illustrate how our approach works. © 2002 Published by Elsevier Science B.V.

We present a logic programming based asynchronous multi-agent system in which agents can communicate with one another; update themselves and each other; abduce hypotheses to explain observations, and use them to generate actions. The knowledge base of the agents is comprised of generalized logic programs, integrity constraints, active rules, and of abducibles. We characterize the interaction among agents via an asynchronous transition rule system, and provide a stable models based semantics. An example is developed to illustrate how our approach works.

We-propose a model checking scheme for a semantically complete fragment of CTL by combining techniques from constraint logic programming, a restricted form of constructive negation and tabled resolution. Our approach is symbolic in that it encodes and manipulates sets of states using constraints, it supports local model checking using goal-directed computation enhanced by tabulation. The framework is parameterized by the constraint domain and supports any finite constraint domain closed under disjunction, projection and complementation. We show how to encode our fragment of CTL in constraint logic programming, we outline an abstract execution model for the resulting type of programs and provide a preliminary evaluation of the approach.

This report addresses the problem of fault propagation between software modules in a large industrial control system with anobject oriented architecture. There exists a conflict between object-oriented design goals such as encapsulation and modularity, and the possibility to suppress propagating error conditions. When an object detects an error condition, it is not desirable toperform the extensive querying of other objects that would be necessary to decide how close to the real fault the object is and hence whether it should report to the user. The fault propagation manifests itself as many irrelevant error messages thus causing problems for system operators and service personnel trying to quickly isolate the real fault. A system developer with insight in the system design, can, of course, often easily interpret the multitude of error messages from a fault scenario and isolate the primary cause. The key observation is thatt his can often be done using high-level models of the system and the fault propagation. We have made an effort to automate this procedure, and we propose a fault isolation scheme as an extra layer between the operator and the core control system. In the fault isolation layer, post-processing of the fault information from the system is performed, to achieve clear and concise fault information to the operator without violating encapsulation and modularity. A high-level and informal explanation model for the fault propagation is presented and a taxonomy for error conditions in an object oriented system is proposed. We outline algorithms and methods that use the explanation model and the error condition taxonomy together with a structural system model to form a cause-effect relation on the error messages, that can be used to find the most significant error message(s) in a fault scenario.The approach is illustrated by means of several examples. The approach has been implemented and tested on a commercial control system for industrial robots developed by ABB Robotics. A patent claim has also been filed with the Swedish Patent Office (PRV).

Magic sets and, more recently, magic templates have been used in the field of deductive databases to facilitate efficient bottom-up evaluation of database queries. Roughly speaking a top-down computation of a definite logic program is simulated by first transforming the program and then executing the new program bottom-up. In this paper we give a new and very simple proof that this approach is equivalent to the collecting interpretation of the abstract interpretation framework for logic programs of Mellish. As a side-effect we are also able to show that “bottom-up” abstract interpretation based on the magic templates transformation is equally powerful as Mellish's abstract interpretation framework, but less powerful than other (more precise) abstract interpretation frameworks.

A number of constituents of a methodology for the systematic design of abstract machines for logic programming languages are described. By means of partial deduction and other program transformation techniques, an interpreter and a source program are “compiled” into a new residual program consisting of: 1) “machine code” for the source program, and 2) an abstract machine for the machine code. Based upon the appearance of these, the user may choose to refine the original interpreter and repeat the process until the resulting “machine code” and the abstract machine satisfy the user's expectations of an abstract machine. We illustrate these principles by reconstructing several of the control instructions of Warren's Abstract Machine. The paper complements previous work of Kursawe, who reconstructed several of the unification instructions using similar techniques.

Because of the conceptual gap between high-level logic programming languages and existing hardware, the problem of compilation is hard. This thesis addresses two ways of narrowing this gap – program analysis through abstract interpretation and the introduction of intermediate languages and abstract machines.

By means of abstract interpretations it is possible to infer program properties which are not explicitly represented in the program – properties that can be used by a compiler to generate specialized code. We describe a framework for constructing and computing abstract interpretations of logic programs with equality. The core of the framework is an abstract interpretation called the base interpretation which provides a model of the run-time behaviour of the program. The model characterized by the base interpretation consists of the set of all reachable computation states of a transition system specifying an operational semantics reminiscent of SLD-resolution. This model is in general not effectively computable. However, the base interpretation can be used for constructing new abstract interpretations which approximate this model. Our base interpretation combines both a simple and concise formulation. with the ability of inferring a wide range of program properties. The framework supports a variety of computation strategies including, in particular, efficient computing of approximate models using a chaotic iteration strategy.

We also show that abstract interpretations may form a basis for implementation of deductive data bases. We relate the magic templates approach to bottom-up evaluation of deductive databases with the base interpretation of C. Mellish and prove that they not only specify isomorphic models but also that the computations which lead up to those models are isomorphic. This implies that methods (for instance, evaluation and transformation techniques) which are applicable in one of the fields are also applicable in the other. As a side-effect we are also able to relate so-called "top-down" and "bottom-up" abstract interpretations.

Abstract machines and intermediate languages are often used to bridge the conceptual gap between language and hardware. Unfortunately – because of the way they are presented – it is often difficult to see the relationship between the high-level and intermediate language. In the final part of the thesis we propose a methodology for designing abstract machines for logic programming languages in such a way that much of the relationship is preserved throughout the process. Using partial deduction and other transformation techniques, a source program and an interpreter are "compiled" into a new program consisting of "machine code" for the source program and an abstract machine for the machine code. Based upon the appearance of the abstract machine the user may choose to modify the interpreter and repeat the process until the abstract machine reaches a suitable level of abstraction. We demonstrate how these techniques can be applied to derive several of the control instructions of Warren's Abstract Machine, thus complementing previous work by P. Kursawe who reconstructed several of the unification instructions using similar techniques.

The notion of abstract interpretation facilitates a formalized process of approximating meanings of programs. Such approximations provide a basis for inferring properties of programs. After having been used mainly in the area of compiler optimization of traditional, imperative languages it has recently also attracted people working with declarative languages.This thesis provides a systematic framework for developing abstract interpretations of logic programs. The work consists of three major parts which together provide a basis for practical implementations of abstract interpretation techniques. Our starting point is a new semantic description of logic programs which extracts the set of all reachable internal states in a possibly infinite collection of SLD-derivations. This semantics is called the base interpretation. Computationally the base interpretation is of little interest since it is not, in general, effectively computable. The aim of the base interpretation is rather to facilitate construction of abstract interpretations which approximate it. The second part of this work provides systematic methods for constructing such abstract interpretations from the base interpretation. The last part of the thesis concerns efficient computing of approximate meanings of programs. We provide some simple but yet efficient algorithms for computing meanings of programs.

The thesis also provides a survey of earlier work done in the area of abstract interpretation of logic programs and contains a comparison between that work and the proposed solution.

This paper presents an alternative approach to implementation of DCGs. In contrast to the standard implementation we use the well-known bottom-up SLR(1)-parsing technique. An experimental system, AID, based on this technique is presented and discussed. The aim of this work is twofold. Firstly, we describe an alternative principle of implementation of DCGs, which makes it possible to cope with left-recursive DCGs and to avoid unnecessary backtracking when parsing. Secondly, we demonstrate that Prolog can be used for implementation of table driven parsers that generalize deterministic LR(k)-parsing techniques to the case of ambiguous grammars. The parsers generated by our system are deterministic whenever the submitted grammar is SLR(1). Otherwise the shift/reduce or reduce/reduce conflicts are stored in the generalized table and are used as Prolog backtrack points.