Bibliography

[1] Deepak Matthaikutty, David Berner, Hiren Patel, and Sandeep Shukla. SystemCXML. http://systemcxml.sourceforge.net/.
[ bib ]
[2] Dimitri van Heesch. Doxygen. http://www.doxygen.org.
[ bib ]
[3] Edison Design Group. Compiler front ends. http://www.edg.com/.
[ bib ]
[4] Steve Donovan. The UnderC development project. http://home.mweb.co.za/sd/sdonovan/underc.html.
[ bib ]
[5] Cadence Design Systems. NC-SystemC.
http://www.cadence.com/products/functional_ver/nc-systemc/.
[ bib ]
[6] Actis Design, LLC. AccurateC Rule Checker. http://www.actisdesign.com/.
[ bib ]
[7] D. Heuzeroth, T. Holl, and W. Löwe. Combining static and dynamic analyses to detect interaction patterns, 2002. In IDPT, 2002. (submitted to). Welf Löwe and Markus Noga.
[ bib ]
[8] Claudio Riva and Jordi Vidal Rodriguez. Combining static and dynamic views for architecture reconstruction. In European Conference on Software Maintenance and Reengineering, pages 47-56. IEEE Computer Society Press, 2002.
[ bib ]
Static analysis aims at recovering the structure of a software system, while dynamic analysis focuses on its run time behaviour. We propose a technique for combining the analysis of static and dynamic architectural information to support the task of architecture reconstruction. The approach emphasises the correct choice of architecturally significant concepts for the reconstruction process and relies on abstraction techniques for their manipulation. The technique allows the software architect to create a set of architectural views valuable for the architecture description of the system.To support our technique, we outline an environment that relies on hierarchical typed directed graphs to show the system's structure and message sequence charts for its behaviour. The main features of the environment are: visualisation of static and dynamic views, synchronisation of abstractions performed on the views, scripting support and management of the use cases. The approach and the environment are demonstrated with an example.
Keywords: Software Architecture, Reverse Engineering, MSC, Dynamic Analysis, Architecture Reconstruction
[9] Alfred V. Aho, Ravi Sethi, and Jeffrey D. Ullman. Compilers - Principles, Techniques, and Tools. Addison-Wesley, Reading, MA, USA, 1986.
[ bib ]
[10] SPIRIT Consortium. http://www.spiritconsortium.com/.
[ bib ]
[11] Synopsys Inc. CoCentric System Studio.
http://www.synopsys.com/products/cocentric_studio/cocentric_studio.html.
[ bib ]
[12] Wilson Snyder. SystemPerl home page. http://www.veripool.com/systemperl.html.
[ bib ]
[13] Görschwin Fey, Daniel Große, Tim Cassens, Christian Genz, Tim Warode, and Rolf Drechsler. ParSyC: An efficient SystemC parser. In Synthesis And System Integration of Mixed Information technologies, 2004. http://www.informatik.uni-bremen.de/agram/doc/work/04sasimi_parsyc.pdf.
[ bib ]
[14] FZI Forschungszentrum Informatik, Department of Microelectronic System Design. KaSCPar - karlsruhe SystemC parser suite. http://www.fzi.de/sim/kascpar.html.
[ bib ]
[15] Javier Castillo Villar. sc2v: SystemC to verilog synthesizable subset translator. http://www.opencores.org/projects.cgi/web/sc2v/overview.
[ bib ]
[16] Rolf Drechsler and Daniel Große. Formal verification of ltl formulas for systemc designs. riptsizehttp://www.informatik.uni-bremen.de/grp/ag-ram/doc/konf/iscas03_verification_systemc.pdf.
[ bib ]
[17] Open SystemC Initiative. SystemC v2.0.1 Language Reference Manual, 2003. http://www.systemc.org/.
[ bib ]
[18] N. Halbwachs, F. Lagnier, and C. Ratel. Programming and verifying critical systems by means of the synchronous data-flow programming language lustre. IEEE Transactions on Software Engineering, Special Issue on the Specification and Analysis of Real-Time Systems, September 1992.
[ bib ]
[19] B. Jeannet. Dynamic partitioning in linear relation analysis. application to the verification of reactive systems. Formal Methods in System Design, 23(1):5-37, July 2003.
[ bib ]
[20] B. Jeannet. partitionnement Dynamique dans l'Analyse de Relations Linéraires et Application à la Vérification de Programmes Synchrones. PhD thesis, Institut National Polytechnique de Grenoble, September 2000.
[ bib ]
[21] J-L. Bergerand, P. Caspi, N. Halbwachs, D. Pilaud, and E. Pilaud. Outline of a real time data-flow language. In Real Time Systems Symposium, San Diego, September 1985.
[ bib ]
[22] E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM TOPLAS, 8(2), 1986.
[ bib ]
[23] J. P. Queille and J. Sifakis. Specification and verification of concurrent systems in cesar. In International Symposium on Programming. LNCS 137, Springer Verlag, April 1982.
[ bib ]
[24] W. Müler, W. Rosentiel, and J. Ruf. SystemC Methodologies and Applications, chapter 2. Kluwer, 2003.
[ bib ]
[25] Felice Balarin, Luciano Lavagno, Claudio Passerone, Alberto L. Sangiovanni-Vincentelli, Marco Sgroi, and Yosinori Watanabe. Modeling and designing heterogeneous systems. In Concurrency and Hardware Design, Advances in Petri Nets, pages 228-273. Springer-Verlag, 2002.
[ bib ]
[26] ARM Limited. AHB Example Amba SYstem technical reference manual, http://www.arm.com/pdfs/DDI0170A.zip.
[ bib ]
[27] Jim-Moi WONG and Jean-Philippe STRASSEN. EASY platform. STMicroelectronics confidential, May 2004.
[ bib ]
[28] Patrice Godefroid. Model checking for programming languages using VeriSoft. In ACM, editor, Conference record of POPL '97, the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages: papers presented at the symposium, Paris, France, 15-17 January 1997, pages 174-186, New York, NY, USA, 1997. ACM Press.
[ bib | http ]
Keywords: algorithms; design; languages; measurement; performance; theory; verification
[29] T. Bultan. BDD vs. constraint-based model checking: An experimental evaluation for asynchronous concurrent systems. Technical Report ucsb_cs:TR-1999-33, University of California, Santa Barbara, Computer Science, October 6 1999.
[ bib | http ]
BDD-based symbolic model checking has been applied to a wide range of applications. Recently, constraint-based approaches, which use arithmetic constraints as a symbolic representation, have been used in symbolic model checking of infinite-state systems. We argue that use of constraint-based model checking is not limited to infinite-state systems. It can also be an efficient alternative to BDD-based model checking for systems with integer variables that have large domains. In this paper we compare the performance of BDD-based model checker SMV to the performance of our constraint-based model checker on verification of several asynchronous concurrent systems. The results indicate that constraint-based model checking is a viable option for verification of asynchronous concurrent systems that require more than 5 boolean variables to encode each integer variable.
Keywords: symbolic model checking, BDDs, constraint representations, Presburger arithmetic
[30] Tevfik Bultan. Action language: A specification language for model checking reactive systems. March 2000.
[ bib | .ps ]
We present a specification language called Action Language for model checking software specifications. Action Language forms an interface between transition system models that a model checker generates and high level specification languages such as Statecharts, RSML and SCR-similar to an assembly language between a microprocessor and a programming language. We show that Action Language translations of Statecharts and SCR specifications are compact and they preserve the structure of the original specification. Action Language allows specification of both synchronous and asynchronous systems. It also supports modular specifications to enable compositional model checking. Keywords Reactive systems, specification languages, model checking. 1 INTRODUCTION Developing reliable software for reactive systems is one of the most challenging goals in information technology. A reactive system is one which interacts with its environment continuously without terminating [22]. Typical examples ar...
[31] Tevfik Bultan and. Automated symbolic analysis of reactive systems. PhD thesis, research directed by Dept. of Computer Science, 1998.
[ bib ]
[32] Richard Gerber and Tevfik Bultan. Composite model checking with type specific symbolic encodings. March 13 1998.
[ bib | .ps.gz ]
We present a new symbolic model checking technique, which analyzes temporal properties in multityped transition systems. Specifically, the method uses multiple type-specific data encodings to represent system states, and it carries out fixpoint computations via the corresponding type-specific symbolic operations. In essence, different symbolic encodings are unified into one composite model checker. Any type-specific language can be included in this framework - provided that the language is closed under Boolean connectives, propositions can be checked for satisfiability, and relational images can be computed. Our technique relies on conjunctive partitioning of transition relations of atomic events based on variable types involved, which allows independent computation of one-step pre- and post-conditions for each variable type. In this paper we demonstrate the effectiveness of our method on a nontrivial data-transfer protocol, which contains a mixture of integer and Boolean-valued varia...
[33] Richard Gerber Tevfik Bultan and Christopher League. Composite model checking: Verification with type-specific symbolic representations. Technical Report ucsb_cs:TR-1999-02, University of California, Santa Barbara, Computer Science, January 2 1999.
[ bib | http ]
In recent years, there has been a surge of progress in automated verification methods based on state exploration. In areas like hardware design, these technologies are rapidly augmenting key phases of testing and validation. To date, one of the most successful of these methods has been symbolic model checking, in which large finite-state machines are encoded into compact data structures such as binary decision diagrams (BDDs) - and are then checked for safety and liveness properties.

However, these techniques have not realized the same success on software systems. One limitation is their inability to deal with infinite-state programs - even those with a single unbounded integer. A second problem is that of finding efficient representations for various variable types. We recently proposed a model checker for integer-based systems that uses arithmetic constraints as the underlying state representation. While this approach easily verified some subtle, infinite-state concurrency problems, it proved inefficient in its treatment of boolean and (unordered) enumerated types - which are not efficiently representable using arithmetic constraints.

In this paper we present a new technique that combines the strengths of both BDD and arithmetic constraint representations. Our composite model merges multiple type-specific symbolic representations in a single model checker. A system's transitions and fixpoint computations are encoded using both BDD (for boolean and enumerated types), and arithmetic constraint (for integers) representations, where the choice depends on the variable types. Our composite model checking strategy can be extended to other symbolic representations provided that they support operations such as intersection, union, complement, equivalence checking and relational image computations. We also present conservative approximation techniques for composite representations to address the undecidability of model checking on infinite-state systems.

We demonstrate the effectiveness of our approach by analyzing two example systems which include a mixture of booleans, integers and enumerated types. One of them is a requirements specification for the control software of a nuclear reactor's cooling system, and the other one is a transport protocol specification.

Keywords: Symbolic model checking, computer aided verification, software specifications
[34] Edmund Clarke and Daniel Kroening. Hardware verification using ANSI-C programs as a reference. In Proceedings of ASP-DAC 2003, pages 308-311. IEEE Computer Society Press, January 2003.
[ bib ]
[35] Edmund Clarke, Daniel Kroening, and Flavio Lerda. A tool for checking ANSI-C programs. In Kurt Jensen and Andreas Podelski, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004), volume 2988 of Lecture Notes in Computer Science, pages 168-176. Springer, 2004.
[ bib ]
[36] Klaus Havelund. Java pathfinder: A translator from java to promela. September 30 1999.
[ bib | .pdf ]
nterrupts, and perhaps most importantly: thread operations. Among major concepts not translated are: packages, method overloading and overriding, method recursion, strings, and floating point numbers. Finally, the class library is not translated. References
[37] K. Havelund and G. Rosu. Monitoring Java programs with Java PathExplorer. Electronic Notes in Theoretical Computer Science, 55(2):1-18, January 2004.
[ bib ]
[38] Klaus Havelund and Thomas Pressburger. Model checking java programs using java pathfinder. September 12 1999.
[ bib | .ps.Z ]
. This paper describes a translator called Java PathFinder (Jpf), from Java to Promela, the modeling language of the Spin model checker. Jpf translates a given Java program into a Promela model, which then can be model checked using Spin. The Java program may contain assertions, which are translated to similar assertions in the Promela model. The Spin model checker will then look for deadlocks and violations of any stated assertions. Jpf generates a Promela model with the same state space characteristics as the Java program. Hence, the Java program must have a finite and tractable state space. This work should be seen in a broader attempt to make formal methods applicable within NASA's areas such as space, aviation, and robotics. The work is a continuation of an effort to formally analyze, using Spin, a multi-threaded operating system for the Deep-Space 1 space craft, and of previous work in applying existing model checkers and theorem provers to real applications. Key words: Program...
[39] Klaus Havelund, Seungjoon Park, and Willem Visser. Java pathfinder - second generation of a java model checker. May 27 2000.
[ bib | .ps.gz ]
We have been developing an automated abstraction tool, which converts a Java program to an abstract program with respect to user-specified abstraction criteria. The user can specify abstractions by removing variables in the concrete program and/or adding new variables (currently the tool supports adding boolean types only) to the abstract program. Specifically, the user selects variables that must be removed and adds abstract variables that represent the predicates in which these variables occurred (typically the predicates are selected from conditions in if and while statements). Given a Java program and such abstraction criteria, the tool generates an abstract Java program in terms of the new abstract variables and unremoved concrete variables. To compute the conversion automatically, JPF uses a decision procedure, SVC (Stanford Validity Checker), which checks the validity of logical expressions [1]. The abstraction tool is designed for object-oriented programs. The user can sp...
[40] Klaus Havelund. Using runtime analysis to guide model checking of java programs. January 27 2001.
[ bib | .pdf ]
This paper describes how two runtime analysis algorithms, an existing data race detection algorithm and a new deadlock detection algorithm, have been implemented to analyze Java programs. Runtime analysis is based on the idea of executing the program once, and observing the generated run to extract various kinds of information. This information can then be used to predict whether other different runs may violate some properties of interest, in addition of course to demonstrate whether the generated run itself violates such properties. These runtime analyzes can be performed stand-alone to generate a set of warnings. It is furthermore demonstrated how these warnings can be used to guide a model checker, thereby reducing the search space. The described techniques have been implemented in the home grown Java model checker called Java PathFinder.
[41] K. Havelund and G. Rosu. An overview of the runtime verification tool Java PathExplorer: Special issue on selected papers from the First International Workshop on Runtime Verification Held in Paris, July 2001 (RV01). Formal Methods in System Design, 24(2):189-215, March 2004.
[ bib ]
[42] Lionel Blanc, Amar Bouali, Jérôme Dormoy, and Olivier Meunier. A methodology for SoC top-level validation using esterel studio. In Electronic Design Processes, April 2002.
[ bib ]
[43] R. Milner. Calculi for synchrony and asynchrony. Theoretical Computer Science, 25(3):267-310, July 1983.
[ bib ]
Keywords: Abelian group; algebraic theory; asynchrony; bisimulation; calculus; combinatorial switching; combinators; distributed computation; modelling; synchrony
[44] Fabrice Baray, Philippe Codognet, Daniel Diaz, and Henri Michel. Code-based test generation for validation of functional processor descriptions. In TACAS, April 2003.
[ bib ]
[45] E. Jahier, B. Jeannet, F. Gaucher, and F. Maraninchi. Automatic state reaching for debugging reactive programs. In AADEBUG, Ghent, September 2003.
[ bib ]
[46] G. Pace, N. Halbwachs, and P. Raymond. Counter-example generation in symbolic abstract model-checking. In FMICS'2001, Paris, July 2001. Inria.
[ bib ]
[47] P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL'77, Los Angeles, January 1977.
[ bib ]
[48] T. Sakunkonchak and M. Fujita. Verification of synchronization in SpecC description with the use of difference decision diagrams. In FDL, 2002.
[ bib ]
[49] Giovanni Agosta, Francesco Bruschi, and Donatella Sciuto. Static analysis of transaction-level models. In DAC, June 2003.
[ bib ]
[50] Thomas Ball and Sriram K. Rajamani. Boolean programs: A model and process for software analysis. Technical report, Microsoft Research, February 2000.
[ bib ]
[51] K. L. McMillan. Symbolic Model Checking. PhD thesis, Boston, 1993.
[ bib ]
[52] Kenneth L. McMillan. Getting started with SMV. Cadence Berkeley Labs, Berkeley, CA 94704 USA, 2001.
[ bib ]
[53] K. L. McMillan. The SMV system, November 06 1992.
[ bib | .ps.gz ]
This document describes the syntax and semantics of the SMV input language, and the function of the SMV model checker. It also describes some optional features of the model checker which can be used to fine tune the performance, and gives some examples of its application. All of the examples in this document are made available with the software. For a description of all the model checker options, see the UNIX programmer's manual entry for SMV, which is also included with the software
[54] K. L. McMillan. The SMV language. Technical report, Cadence Berkeley Labs, March 1999.
[ bib ]
[55] F. Maraninchi and Y. Rémond. Argos: an automaton-based synchronous language. Computer Languages, (27):61-92, 2001.
[ bib ]
[56] G. Berry. The foundations of Esterel. Proof, Language and Interaction: Essays in Honour of Robin Milner, 2000. Editors: G. Plotkin, C. Stirling and M. Tofte.
[ bib ]
[57] L. Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering, SE-3(2):125-143, 1977.
[ bib ]
[58] PROVER Technology. Prover plug-in for scade. http://www.prover.com/products/ppi/sl.xml.
[ bib ]
[59] Richard M. Stallman and the GCC developer community. GNU Compiler Collection Internals. Free Software Fundation. http://gcc.gnu.org/onlinedocs/gccint/.
[ bib ]
[60] Ammar Aljer Philippe. BHDL: Circuit design in b, 2003.
[ bib | .html ]
[61] JR Abrial and A Nikolaos. The B-book: assigning programs to meanings. Cambridge University Press New York, NY, USA, 1996. ISBN:0-521-49619-5.
[ bib ]
[62] D. L. Dill, E. M. Clarke, J. R. Burch, K. L. Mcmillan, and L. J. Hwang. Symbolic model checking: 1020 states and beyond, march 1990.
[ bib | .ps.gz ]
Many different methods have been devised for automatically verifying finite state systems by examining state-graph models of system behavior. These methods all depend on decision procedures that explicitly represent the state space using a list or a table that grows in proportion to the number of states. We describe a general method that represents the state space symbolically instead of explicitly. The generality of our method comes from using a dialect of the Mu-Calculus as the primary specification language. We describe a model checking algorithm for Mu-Calculus formulas that uses Bryant's Binary Decision Diagrams (1986) to represent relations and formulas. We then show how our new Mu-Calculus model checking algorithm can be used to derive efficient decision procedures for CTL model checking, satisfiability of linear-time temporal logic formulas, strong and weak observational equivalence of finite transition systems, and language containment for finite !-automata. The fixed point co...
[63] Alain Kerbrat, Amir Pnueli, Anne Rasse, Eugene Asarin, Marius Bozga, and Oded Maler. Data-structures for the verification of timed automata, April 30 1997.
[ bib | .html ]
. In this paper we suggest numerical decision diagrams, a bdd- based data-structure for representing certain subsets of the Euclidean space, namely those encountered in verification of timed automata. Unlike other representation schemes, ndd's are canonical and provide for all the necessary operations needed in the verification and synthesis of timed automata. We report some preliminary experimental results. 1 Introduction Consider a transition system A = (Q; ffi), where Q is the set of states and ffi : Q 7! 2 Q is a transition function, mapping each state q 2 Q into the set of q-successors ffi(q) ` Q. The problem of calculating or characterizing all the states reachable from a subset F ` Q of the state-space is one of the central problems in verification. The basic algorithm to calculate this set of states is the following: F 0 := F for i = 0; 1; : : : ; repeat F i+1 := F i [ ffi(F i ) until F i+1 = F i where ffi(F i ) = S q2F i ffi(q). Symbolic methods [BCM + 93], [M...
[64] Dr. Alain Deutsch. Static verification of dynamic properties. Technical report, PolySpace Technologies, November 2003.
[ bib ]
[65] Erich Gamma, Richard Helm, Ralph Johnson, and John Vlissides. Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, 1994.
[ bib ]
[66] Moshe Y. Vardi. Branching vs. linear time: Final showdown. In TACAS 2001: Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 1-22, London, UK, 2001. Springer-Verlag.
[ bib ]
[67] A. Pnueli. The temporal logic of programs. Technical report, Jerusalem, Israel, Israel, 1997.
[ bib ]
[68] John Ellson, Emden Gansner, Lefteris Koutsofios, Stephen C. North, and Gordon Woodhull. Graphviz - open source graph drawing tools. In Lecture Notes in Computer Science, volume Volume 2265 / 2002, page 483. Springer-Verlag GmbH, July 2003.
[ bib ]
[69] N. Halbwachs, F. Lagnier, and P. Raymond. Synchronous observers and the verification of reactive systems. In M. Nivat, C. Rattray, T. Rus, and G. Scollo, editors, Third Int. Conf. on Algebraic Methodology and Software Technology, AMAST'93, Twente, June 1993. Workshops in Computing, Springer Verlag.
[ bib ]
[70] N. Halbwachs and S. Baghdadi. Synchronous modeling of asynchronous systems. In EMSOFT'02, Grenoble, October 2002. LNCS 2491, Springer Verlag.
[ bib ]
[71] Marius Bozga, Susanne Graf, Iulian Ober, Ileana Ober, and Joseph Sifakis. The if toolset. In 4th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Real Time, SFM-04:RT, Bologna, Sept. 2004, LNCS Tutorials, Springer, 2004.
[ bib ]
[72] O. Coudert, C. Berthet, and J. C. Madre. Verification of synchronous sequential machines based on symbolic execution. In Proceedings of the international workshop on Automatic verification methods for finite state systems, pages 365-373, New York, NY, USA, 1990. Springer-Verlag New York, Inc.
[ bib ]
[73] Randal E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293-318, 1992.
[ bib | .html ]
[74] Frank (Ed.) Ghenassia, editor. Transaction-Level Modeling with SystemC. TLM Concepts and Applications for Embedded Systems. Springer, June 2005. ISBN 0-387-26232-6.
[ bib ]
[75] Adam Rose, Stuart Swan, John Pierce, Jean-Michel Fernandez, and Cadence Design Systems. Transaction level modeling in systemc. Technical report, Mentor Graphics; Cadence Design Systems, 2005.
[ bib ]
[76] Sudeep Pasricha. Transaction level modeling of SoC in systemc 2.0. Technical report, STMicroelectronics Ltd, 2002.
[ bib ]
[77] Lukai Cai and Daniel Gajski. Transaction level modeling: an overview. In CODES+ISSS '03: Proceedings of the 1st IEEE/ACM/IFIP international conference on Hardware/software codesign and system synthesis, pages 19-24, New York, NY, USA, 2003. ACM Press.
[ bib ]
[78] Matthieu Moy, Florence Maraninchi, and Laurent Maillet-Contoz. Pinapa: An extraction tool for systemc descriptions of systems-on-a-chip. In EMSOFT, September 2005.
[ bib ]
[79] Matthieu Moy, Florence Maraninchi, and Laurent Maillet-Contoz. LusSy: A toolbox for the analysis of systems-on-a-chip at the transactional level. In International Conference on Application of Concurrency to System Design, June 2005.
[ bib ]
[80] A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu. Symbolic model checking using SAT procedures instead of BDDs, September 10 1999.
[ bib | .ps.gz ]
In this paper, we study the application of propositional decision procedures in hardware verification. In particular, we apply bounded model checking, as introduced in [1], to equivalence and invariant checking. We present several optimizations that reduce the size of generated propositional formulas. In many instances, our SAT-based approach can significantly outperform BDD-based approaches. We observe that SAT-based techniques are particularly efficient in detecting errors in both combinational and sequential designs. 1 Introduction A complex hardware design can be error-prone and mistakes are costly. Formal verification techniques such as symbolic model checking are gaining wide industrial acceptance. Compared to traditional validation techniques based on simulation, they provide more extensive coverage and can detect subtle errors. Representing and manipulating boolean expressions is critical to many formal verification techniques. BDDs [3] have traditionally been used for this p...
[81] Muhammad Muzammil Shahbaz. Automatic verification techniques for system-on-chip using symbolic model verifier. Master's thesis, Université Joseph Fourier, Grenoble, France, June 2005. Work performed in Verimag.
[ bib ]
[82] Florence Maraninchi and Fabien Gaucher. Step-wise + algorithmic debugging for reactive programs: Ludic, a debugger for lustre. In Automated and Algorithmic Debugging, 2000.
[ bib | .html ]
[83] Jacomme Ludovic Dunoyer Julien, Pétrot Frédéric. Intrinsic limitations of logarithmic encodings for low power finite state machines. In Mixed Design of VLSI Circuits Conference, pages 613-618, June 1997.
[ bib ]
[84] Marius Bozga, Jean-Claude Fernandez, and Lucian Ghirvu. State space reduction based on live variables analysis. In Agostino Cortesi and Gilberto Filé, editors, Static Analysis, volume 1694 of Lecture Notes in Computer Science, pages 164-178. Springer, 1999.
[ bib ]
[85] G. J. Chaitin. Register allocation and spilling via graph coloring. ACM SIGPLAN Notices, 17(6):98-105, June 1982.
[ bib ]
Keywords: global register allocation; graph coloring; graph colouring; machine registers; PL/I; PL/I optimizing compiler; program compilers; register conflict graph; spill code
[86] Frank Mueller. Register allocation by graph coloring: A review, April 14 1993.
[ bib | .ps.gz ]
Introduction The problem of register allocation for code generation can be described as follows: Given a set of (hardware) registers, what is the most efficient mapping of registers to program variables in terms of execution time of the program. But let us first define some terms to describe the problem more formally. A variable is defined at a point in a program when a value is assigned to it. A variable is used at a point in a program when its value is referenced in an expression. A variable is said to be live at a point if it has been defined earlier and will be used later. The live range of a variable is the execution range (a set of adjacent vertices of the control flow graph of the program) between definitions and uses of a variable. Two variables are simultaneously live if and only if both are live for the a vertex v of the control flow graph. A proper register allocation<
[87] Dirk Hoffmann, Joachim Gerlach, Juergen Ruf, Thomas Kropf, Wolfgang Mueller, and Wolfgang Rosenstiehl. The simulation semantics of systemC, December 21 2001.
[ bib | .ps.Z ]
We present a rigorous but transparent semantics definition of SystemC that covers method, thread, and clocked thread behavior as well as their interaction with the simulation kernel process. The semantics includes watching statements, signal assignment, and wait statements as they are introduced in SystemC V1.0. We present our definition in form of distributed Abstract State Machines (ASMs) rules reflecting the view given in the SystemC User's Manual and the reference implementation. We mainly see our formal semantics as a concise, unambiguous, high-level specification for SystemC-based implementations and for standardization. Additionally, it can be used as a sound basis to investigate SystemC interoperability with Verilog and VHDL. 1. Introduction SystemC is the emerging de-facto-standard for systemlevel modeling and design from the Open SystemC Initiative (OSCI) which is controlled by a steering group and backed by a growing community of currently over 50 charter member companies...
[88] Ashraf Salem. Formal semantics of synchronous systemc. In DATE, pages 10376-10381, 2003.
[ bib ]
[89] Guido Arnout (CoWare, Inc.). C for system level design, September 1999. https://www.systemc.org/projects/sitedocs/document/coWare/en/1.
[ bib ]
[90] Masahiro Fujita and Hiroshi Nakamura. The standard specc language. In ISSS, pages 81-86, 2001.
[ bib | .html ]
[91] Gopi Ganapathy, Ram Narayan, Glenn Jorden, Denzil Fernandez, Ming Wang, and Jim Nishimura. Hardware emulation for functional verification of K5. 1996.
[ bib | http ]
[92] Daniel Kroening and Natasha Sharygina. Formal verification of systemc by automatic hardware/software partitioning. In Proceedings of MEMOCODE 2005, pages 101-110. IEEE, 2005.
[ bib ]
[93] S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In O. Grumberg, editor, Proc. 9th INternational Conference on Computer Aided Verification (CAV'97), volume 1254, pages 72-83. Springer Verlag, 1997.
[ bib | .html ]
[94] Nicolas Palix. Modélisation et vérification de systèmes sur puces à base de composants. Master's thesis, ESISAR/INPG, Grenoble, France, 2004.
[ bib ]
[95] Yvan Roux. Rapport intermédiaire du projet vercors. Internal report in INRIA Rhône Alpes, June 2005.
[ bib ]
[96] Prometheus - A compositional modeling tool for real-time systems, September 25 2001.
[ bib | .ps ]
Prometheus is a modeling tool allowing the user to specify and compose real-time systems, by means of synchronization and priorization of actions, with a scheduler specified in a high-level description language. The resulting model is checked for consistency of the priorities, safety and liveness properties which can - up to a certain degree - be guaranteed by Prometheus. The composed system can be output in several formats.
[97] Yves Bertot and Pierre Casteran. Interactive Theorem Proving and Program Development. SpringerVerlag, 2004.
[ bib ]
[98] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002.
[ bib ]
[99] S. Owre, J. M. Rushby, , and N. Shankar. PVS: A prototype verification system. In Deepak Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 748-752, Saratoga, NY, jun 1992. Springer-Verlag.
[ bib | http ]
[100] Pei-Hsin Ho, Thomas Shiple, Kevin Harer, James Kukula, Robert Damiano, Valeria Bertacco, Jerry Taylor, and Jiang Long. Smart simulation using collaborative formal and simulation engines. pages 120-126.
[ bib ]
[101] Cadence. Formal Verification Using Affirma FormalCheck, October 1999.
[ bib ]
[102] Ilan Beer, Shoham Ben-David, Cindy Eisner, and Avner Landver. RuleBase: an industry-oriented formal verification tool. In 33rd Design Automation Conference (DAC'96), pages 655-660, New York, June 1996. Association for Computing Machinery.
[ bib ]

This file has been generated by bibtex2html 1.75