staticanalysis has gained much attention over the past few years in applications such as bug finding and programverification. As software becomes more complex and componentized, it is common for software systems and...
详细信息
ISBN:
(纸本)1595932631
staticanalysis has gained much attention over the past few years in applications such as bug finding and programverification. As software becomes more complex and componentized, it is common for software systems and applications to be implemented in multiple languages. There is thus a strong need for developing analysis tools for multi-language software. We introduce a technique called analysis Preserving Language Transformation (APLT) that enables the analysis of multi-language software, and also allows analysis tools for one language to be applied to programs written in another. APLT preserves data and control flow information needed to perform static analyses, but allows the translation to deviate from the original program's semantics in ways that are not pertinent to the particular analysis. We discuss major technical difficulties in building such a translator, using a C-to-Java translator as an example. We demonstrate the feasibility and effectiveness of APLT using two usage cases: analysis of the Java runtime native methods and reuse of Java analysis tools for C. Our preliminary results show that a control- and data-flow equivalent model for native methods can eliminate unsoundness and produce reliable results, and that APLT enables seamless reuse of analysis tools for checking high-level program properties. Copyright 2006 ACM.
We address the problem of error detection for programs that take recursive data structures and arrays as input. Previously we proposed a combination of symbolic execution and modelchecking for the analysis of such pr...
详细信息
An internetware application is composed by existing individual services, while transaction processing is a key mechanism to make the composition reliable. The existing research of transactional composite service (TCS...
详细信息
An internetware application is composed by existing individual services, while transaction processing is a key mechanism to make the composition reliable. The existing research of transactional composite service (TCS) depends on the analysis to composition structure and exception handling mechanism in order to guarantee the relaxed atomicity. However, this approach cannot handle some application-specific requirements and causes lots of unnecessary failure recoveries or even aborts. In this paper, we propose a relaxed transaction model, including system mode, relaxed atomicity criterion, staticchecking algorithm and dynamic enforcement algorithm. Users are able to define different relaxed atomicity constraint for different TCS according to application-specific requirements, including acceptable configurations and the preference order. The checking algorithm determines whether the constraint can be guaranteed to be satisfied. The enforcement algorithm monitors the execution and performs transaction management work according to the constraint. Compared to the existing work, our approach can handle complex application requirements, avoid unnecessary failure recoveries and perform the transaction management work automatically.
modelchecking techniques have proven effective for checking a number of non-trivial concurrent object-oriented software systems. However, due to the high computational and memory costs, a variety of model reduction t...
详细信息
We define a new fixpoint modal logic, the visibly pushdown mu-calculus (VP-mu), as an extension of the modal mu-calculus. The models of this logic are execution trees of structured programs where the procedure calls a...
详细信息
We define a new fixpoint modal logic, the visibly pushdown mu-calculus (VP-mu), as an extension of the modal mu-calculus. The models of this logic are execution trees of structured programs where the procedure calls and returns are made visible. This new logic can express pushdown specifications on the model that its classical counterpart cannot, and is motivated by recent work on visibly pushdown languages [4]. We show that our logic naturally captures several interesting program specifications in programverification and dataflow analysis. This includes a variety of program specifications such as computing combinations of local and global program flows, pre/post conditions of procedures, security properties involving the context stack, and interprocedural dataflow analysis properties. The logic can capture flow-sensitive and interprocedural analysis, and it has constructs that allow skipping procedure calls so that local flows in a procedure can also be tracked. The logic generalizes the semantics of the modal mu-calculus by considering summaries instead of nodes as first-class objects, with appropriate constructs for concatenating summaries, and naturally captures the way in which pushdown models are model-checked. The main result of the paper is that the model-checking problem for VP-mu, is effectively solvable against pushdown models with no more effort than that required for weaker logics such as CTL. We also investigate the expressive power of the logic VP-mu: we show that it encompasses all properties expressed by a corresponding pushdown temporal logic on linear structures (CARET [2]) as well as by the classical mu-calculus. This makes VP-mu the most expressive known program logic for which algorithmic softwaremodelchecking is feasible. In fact, the decidability of most known program logics (mu-calculus, temporal logics LTL and CTL, CARET, etc.) can be understood by their interpretation in the monadic second-order logic over trees. This is not true for th
The proceedings contain 36 papers. The special focus in this conference is on software, Formal Methods Tools, Hybrid Systems, Parameterized Systems and Efficient model-checking. The topics include: On the construction...
ISBN:
(纸本)3540672826
The proceedings contain 36 papers. The special focus in this conference is on software, Formal Methods Tools, Hybrid Systems, Parameterized Systems and Efficient model-checking. The topics include: On the construction of automata from linear arithmetic constraints;an extensible type system for component-based design;viewpoint-oriented software development;tool support for integrating multiple perspectives by distributed graph transformation;an architecture for interactive program provers;on memory-block traversal problems in model-checking timed systems;symbolic modelchecking for rectangular hybrid systems;efficient data structure for fully symbolic verification of real-time software systems;verification of parameterized systems using logic program transformations;abstracting ws1s systems to verify parameterized networks;a tool for expressing validation techniques over infinitestate systems;transitive closures of regular relations for verifying infinite-state systems;using staticanalysis to improve automatic test generation;efficient diagnostic generation for Boolean equation systems;compositional state space generation with partial order reductions for asynchronous communicating systems;checking for CFFD-preorder with tester processes;integrating low level symmetries into reachability analysis;modelchecking support for the ASM high-level language;combining constraint solvers with BDDS for automatic invariant checking;symbolic reachability analysis based on sat-solvers;symbolic representation of upward-closed sets;an experimental evaluation for asynchronous concurrent systems and tool-based specification of visual languages and graphic editors.
The proceedings contain 17 papers. The special focus in this conference is on Invited Talk and Tutorials. The topics include: Algebraic specification and program development by stepwise refinement extended abstract;pr...
ISBN:
(纸本)3540676287
The proceedings contain 17 papers. The special focus in this conference is on Invited Talk and Tutorials. The topics include: Algebraic specification and program development by stepwise refinement extended abstract;proof obligations of the b formal method;constraint logic programming applied to modelchecking;on dynamic aspects of OOD frameworks in component-based software development in computational logic;infinitestatemodelchecking by abstract interpretation and program specialisation;mode analysis domains for typed logic programs;imperative program specialisation;specialising finite domain programs using polyhedra;roles of program extension;transformation of left terminating programs;transformation rules for logic programs with goals as arguments;making mercury programs tail recursive;the replacement operation for CCP programs;annotations for prolog - a concept and runtime handling;verification by testing for recursive program schemes;combined static and dynamic assertion-based debugging of constraint logic programs and context-moving transformations for function verification.
Previous work has shown that program slicing can be a useful step in model-checkingsoftware systems. We are interested in applying these techniques to construct models of multi-threaded Java programs. Past work does ...
详细信息
ISBN:
(纸本)3540664599
Previous work has shown that program slicing can be a useful step in model-checkingsoftware systems. We are interested in applying these techniques to construct models of multi-threaded Java programs. Past work does not address the concurrency primitives found in Java, nor does it provide the rigorous notions of slice correctness that are necessary for reasoning about programs with non-deterministic behaviour and potentially infinite computation traces. In this paper, we define the semantics of a simple multi-threaded language with concurrency primitives matching those found in the Java Virtual Machine, we propose a bisimulation-based notion of correctness for slicing in this setting, we identify notions of dependency that are relevant for slicing multi-threaded Java programs, and we use these dependencies to specify a program slicer for the language presented in the paper. Finally, we discuss how these dependencies can be refined to take into account common programming idioms of concurrent Java software.
This volume contains the proceedings of the 11th International Conference on Veri?cation, modelchecking, and Abstract Interpretation (VMCAI 2010), held in Madrid, Spain, January 17–19, 2010. VMCAI 2010 was the 11th ...
详细信息
ISBN:
(数字)9783642113192
ISBN:
(纸本)9783642113185
This volume contains the proceedings of the 11th International Conference on Veri?cation, modelchecking, and Abstract Interpretation (VMCAI 2010), held in Madrid, Spain, January 17–19, 2010. VMCAI 2010 was the 11th in a series of meetings. Previous meetings were held in Port Je?erson (1997), Pisa (1998), Venice (2002), New York (2003), Venice(2004),Paris(2005),Charleston(2006),Nice(2007),SanFrancisco(2008), and Savannah (2009). VMCAI centers on state-of-the-art research relevant to analysis of programs and systems and drawn from three research communities: veri?cation, modelchecking, and abstract interpretation. A goal is to facilitate interaction, cro- fertilization, and the advance of hybrid methods that combine two or all three areas. Topics covered by VMCAI include program veri?cation, program cert- cation, modelchecking, debugging techniques, abstract interpretation, abstract domains, staticanalysis, type systems, deductive methods, and optimization. The program Committee selected 21 papers out of 57 submissions based on anonymous reviews and discussions in an electronic program Committee me- ing. The principal selection criteria were relevance and quality.
This volume contains the proceedings of the 10th International Conference on Veri?cation, modelchecking, and Abstract Interpretation (VMCAI 2009), held in Savannah, Georgia, USA, January 18–20, 2009. VMCAI 2009 was ...
详细信息
ISBN:
(数字)9783540939009
ISBN:
(纸本)9783540938996
This volume contains the proceedings of the 10th International Conference on Veri?cation, modelchecking, and Abstract Interpretation (VMCAI 2009), held in Savannah, Georgia, USA, January 18–20, 2009. VMCAI 2009 was the 10th in a series of meetings. Previous meetings were heldinPortJe?erson1997,Pisa1998,Venice2002,NewYork2003,Venice2004, Paris 2005, Charleston 2006, Nice 2007, and San Francisco 2008. VMCAI centers on state-of-the-art research relevant to analysis of programs and systems and drawn from three research communities: veri?cation, modelchecking, and abstract interpretation. A goal is to facilitate interaction, cro- fertilization, and the advance of hybrid methods that combine two or all three areas. Topics covered by VMCAI include program veri?cation, program cert- cation, modelchecking, debugging techniques, abstract interpretation, abstract domains, staticanalysis, type systems, deductive methods, and optimization. The program Committee selected 24 papers out of 72 submissions based on anonymous reviews and discussions in an electronic program Committee me- ing. The principal selection criteria were relevance and quality. VMCAI has a tradition of inviting distinguished speakers to give talks and tutorials. This time the program included three invited talks by: – E. Allen Emerson (University of Texas at Austin) on “modelchecking: Progress and Problems” – Aarti Gupta (NEC Labs, Princeton) on “modelchecking Concurrent programs” – Mooly Sagiv (Tel-Aviv University) on “Thread Modular Shape analysis” There were also two invited tutorials by: – Byron Cook (Microsoft Research, Cambridge) on “Proving program Ter- nation and Liveness” – V´ eroniqueCortier (LORIA, CNRS, Nancy) on“Veri?cationof Security P- tocols”.
暂无评论