, Modern compiler implementation in ML, 1998.
DOI : 10.1017/CBO9780511811449
, The temporal logic sugar, 13th International Conference on Computer Aided Verification (CAV'01), volume 2102 of Lecture Notes in Computer Science, pp.363-367, 2001.
, Constraints specification at higher levels of abstraction, Proceedings of the IEEE International High Level Design Validation and Test Workshop (HLDVT'01), 2001.
, Symbolic model checking using SAT procedure instead of BDDs, Proceedings of the 36th Design Automation Conference (DAC'99), pp.317-320, 1999.
, A static analyzer for large safety-critical software, Conference on Programming Language Design and Implementation (PLDI'03), pp.196-207, 2003.
, Symbolic model checking for sequential circuit verification, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol.13, issue.4, pp.401-424, 1994.
, Clean formal semantics for VHDL Metropolis: An integrated electronic system design environment, The European Conference on Design, pp.45-52, 2003.
, Bounded model checking using satisfiability solving, Formal Methods in System Design, vol.19, issue.1, pp.7-34, 2001.
DOI : 10.1023/A:1011276507260
, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.238-252, 1977.
DOI : 10.1145/512950.512973
URL : https://hal.archives-ouvertes.fr/inria-00528590
, Constructive versions of Tarski's fixed point theorems, Pacific Journal of Mathematics, vol.81, issue.1, pp.43-57, 1979.
, Systematic design of program analysis frameworks, Conference Record of the 6th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.269-282, 1979.
, Abstract Interpretation Frameworks, Journal of Logic and Computation, vol.2, issue.4, pp.511-547, 1992.
DOI : 10.1093/logcom/2.4.511
, Design and synthesis of synchronization skeletons using branching time temporal logic, Proceedings of the Workshop on Logics of Programs, pp.52-71, 1981.
DOI : 10.1007/BFb0025774
, Automatic verification of finite state concurrent system using temporal logic specifications, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '83, 1983.
DOI : 10.1145/567067.567080
, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '78, 1978.
DOI : 10.1145/512760.512770
, The mathematical foundation of symbolic trajectory evaluation Behavioral consistency of C and verilog programs using bounded model checking, 11th International Conference on Computer Aided Verification (CAV'99), volume 1633 of Lecture Notes in Computer Science Proceedings of the 40th Design Automation Conference (DAC'03), pp.196-207, 1999.
, Taylor expansion diagrams: a compact, canonical representation with applications to symbolic verification, Proceedings 2002 Design, Automation and Test in Europe Conference and Exhibition, pp.285-291, 2002.
DOI : 10.1109/DATE.2002.998286
URL : https://hal.archives-ouvertes.fr/lirmm-00268497
, High-level architectural co-simulation using Esterel and C, Proceedings of the 9th International Symposium on Hardware/Software Codesign (CODES'01), pp.189-194, 2001.
, Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique de programmes Semantic foundations of program analysis, Cou81] P. Cousot Program Flow Analysis: Theory and Applications, chapter 10, pp.303-342, 1978.
, The calculational design of a generic abstract interpreter, Calculational System Design. NATO ASI Series F. IOS Press, 1999.
, A qualitative finite subset of VHDL and semantics, 1993.
, Semantics of a verification-oriented subset of VHDL, Correct Hardware Design and Verification Methods (CHARME'95) 2nd Workshop on Libraries, Component Modeling and Quality Assurance, pp.293-310, 1995.
DOI : 10.1007/3-540-60385-9_18
, Early analysis tools for System-on-a-chip design, IBM Journal of Research and Development, issue.6, pp.46691-707, 2002.
, Guarded commands, nondeterminacy and formal derivation of programs, Communications of the ACM, vol.18, issue.8, pp.453-457, 1975.
, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '82, pp.207-212, 1982.
DOI : 10.1145/582153.582176
, A Computing Procedure for Quantification Theory, Journal of the ACM, vol.7, issue.3, pp.201-215, 1960.
DOI : 10.1145/321033.321034
, Model Checking VHDL with CV, Proceedings of the 2nd International Conference on Formal Methods in Computer-Aided Design (FM- CAD'98, pp.508-514, 1998.
DOI : 10.1007/3-540-49519-3_33
, Electronic Industries Association) Electronic Design Interchange Format (EDIF) Version 3 0 0 Level 0 Reference Manual, 1993.
, A symbolic relation for a subset of VHDL'87 descriptions and its application to symbolic model checking, Correct Hardware Design and Verification Methods (CHARME'95), pp.328-342, 1995.
, Abstract interpretation-based static analysis of mobile ambients, Static Analysis Symposium (SAS'01), pp.412-430, 2001.
, Static analysis of digital filters Functional semantics for deltadelay VHDL based on focus, 13th European Symposium on Programming Formal Semantics for VHDL, pp.33-48, 1995.
, Unifying traditional and formal verification through property checking Set manipulation with boolean functional vectors for symbolic reachability analysis, Designing Correct Circuits Design , Automation and Test in Europe Conference and Exposition (DATE'03), pp.10816-10821, 2002.
, Symbolic simulation, model checking and abstraction with partially ordered boolean function vectors, Computer-Aided Verification, 2004.
DOI : 10.1007/978-3-540-27813-9_20
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.4.4656
, A framework for VHDL combining theorem proving and symbolic simulation, Proceedings of the 3rd International Workshop on the ACL2 Theorem Prover and its Applications (ACL2'02), pp.6-14, 2002.
URL : https://hal.archives-ouvertes.fr/hal-01375425
, A formal model of several fundamental VHDL concepts, Proceedings of the 9th Annual Conference on Computer Assurance (COMPASS'94), pp.177-181, 1994.
, Reasoning about VHDL using operational and observational semantics The semantic challenge of verilog HDL, Correct Hardware Design and Verification Methods (CHARME'95) Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science (LICS'95), pp.311-327, 1995.
, Static analysis of linear congruence equalities among variables of a program Improving the results of static analyses programs by local decreasing iteration, Proceedings of the International Joint Conference on Theory and Practice of Software Development (TAPSOFT'91 Foundations of Software Technology and Theoretical Computer Science (FSTTCS'92), pp.169-192, 1991.
, Vis: A system for verification and synthesis, 8th International Conference on Computer Aided Verification (CAV'96), pp.428-432, 1996.
, An efficient general iterative algorithm for dataflow analysis, Acta Informatica, vol.24, issue.6, pp.679-694, 1987.
DOI : 10.1007/BF00282621
, Positive Boolean Functions as Multiheaded Clauses, 17th International Conference in Logic Programming (ICLP'01), pp.120-134, 2001.
DOI : 10.1007/3-540-45635-X_16
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.13.9743
, Static Analysis of Gated Data Dependence Graphs, 11th International Static Analysis Symposium, 2003.
DOI : 10.1007/978-3-540-27864-1_16
, Checking safety properties of behavioral VHDL descriptions by abstract interpretation, 9th International Static Analysis Symposium (SAS'02), volume 2477 of Lecture Notes in Computer Science, 2002.
, Modular analysis of circuit description language by abstract interpretation: Application to the automatic extraction of circuit shapes, Designing Correct Circuits (DCC'02, 2002.
, International Technology Roadmap for Semiconductors Available at: http://public.itrs, 2003.
, Formal hardware verification by symbolic trajectory evaluation Exponential trends in the integrated circuit industry, 1997.
, Affine relationships among variables of a program, Acta Informatica, vol.6, 1976.
, A unified approach to global program optimization, 1st ACM Symposium on Principles of Programming Languages, pp.194-206, 1973.
, Symbolic RTL simulation, Proceedings of the 38th conference on Design automation , DAC '01, pp.47-52, 2001.
DOI : 10.1145/378239.378278
, Introduction to Metamathematics, 1952.
, VHDLtranslation for BDD-based formal verification, 1994.
, The Objective Caml system release 3.06, documentation and user's manual, Institut National de Recherche en Informatique et en Automatique (INRIA), 2002.
, Checking that finite state concurrent programs satisfy their linear specification, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '85, 1985.
DOI : 10.1145/318593.318622
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.467.2053
, Abstract interpretation using TDGs, Static Analysis Symposium, pp.363-379, 1994.
, The semantics of behavioral VHDL'93 descriptions, Proceedings of the European Design Automation Conference (EURO-DAC'94), pp.500-505, 1994.
, Verification strategy for integration 3G baseband SoC, Proceedings of the 40th conference on Design automation , DAC '03, pp.7-10, 2003.
DOI : 10.1145/775832.775835
, Boolean decomposition using twoliteral divisors, 17th International Conference on VLSI Design (VLSI Design 2004), pp.765-768, 2004.
, Microelectronics Development for European Applications ) Design Automation Solutions for Europe, 2002.
, Operational and algebraic semantics of concurrent processes In Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, pp.1201-1242, 1990.
, A new numerical abstract domain based on difference-bound matrices, Programs as Data Objects (PADO'02), pp.155-172, 2001.
, A few graph-based relational numerical abstract domains, Static Analysis Symposium (SAS'02), pp.117-132, 2002.
, Chaff: Engineering an efficient SAT solver, Proceedings of the 38th Design Automation Conference (DAC'01, 2001.
, System-on-chip beyond the nanometer wall, Proceedings of the 40th conference on Design automation , DAC '03, pp.419-424, 2003.
DOI : 10.1145/775832.775943
, A structural approach to operational semantics, 1981.
, The temporal logic of programs, 18th IEEE Symposium on Foundations of Computer Science, pp.46-57, 1977.
, An Abstract Interpretation Approach for Automatic Generation of Polynomial Invariants, 11th Static Analysis Symposium (SAS'04), Lecture Notes in Computer Science, 2004.
DOI : 10.1007/978-3-540-27864-1_21
, Polynomial Codes Over Certain Finite Fields, Journal of the Society for Industrial and Applied Mathematics, vol.8, issue.2, pp.300-304, 1960.
DOI : 10.1137/0108018
, A formalization of a subset of VHDL in the Boyer-Moore logic. Formal Methods in System Design, pp.7-25, 1995.
, Specification and verification of gate-level VHDL models of synchronous and asynchronous circuits, 1995.
, Formal verification by symbolic evaluation of partially-ordered trajectories, Formal Methods in System Design, vol.6, issue.No. 5, pp.147-189, 1995.
DOI : 10.1007/BF01383966
, Two variables per linear inequality as an abstract domain, Logic Based Program Synthesis and Tranformation (LOPSTR'02), pp.71-89, 2002.
, A Higher-Level Language for Hardware Synthesis, Correct Hardware Design and Verification Methods, pp.228-243, 2001.
DOI : 10.1007/3-540-44798-9_20
, Non-linear loop invariant generation using gröbner bases, Proceedings of the 31st Symposium on Principles of Programming Languages (POPL'04), pp.318-329, 2004.
, Checking Safety Properties Using Induction and a SAT-Solver, 3rd International Conference On Formal Methods in Computer Aided Design (FMCAD'00), volume 1954 of Lecture Notes in Computer Science, 2000.
DOI : 10.1007/3-540-40922-X_8
, Three notes on the interpretation of verilog, 2000.
, FEMTO-VHDL: The semantics of a subset of VHDL and its embedding in the hol proof assistant, 1993.
, Structural operational semantics for a portable subset of behavioral VHDL-93. Formal Methods in System Design, pp.69-88, 2001.
, An MPEG-2 decoder case study as a driver for a system level design methodology, Proceedings of the seventh international workshop on Hardware/software codesign , CODES '99, 1999.
DOI : 10.1145/301177.301196
, An automata-theoretic approach to automatic program verification, 1st Annual Symposium on Logic in Computer Science (LICS'86), 1986.
DOI : 10.1007/3-540-50403-6_33
, Symbolic Simulation with Approximate Values, Formal Methods in Computer- Aided Design, pp.470-485, 1954.
DOI : 10.1007/3-540-40922-X_29
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.9762
, Compiler design, 1995.
DOI : 10.1007/978-3-642-17540-4
, Yet another ensemble of abstract interpreter, higherorder data-flow equations, and model checking, 2001.