[ICE12] L.PIERRE: "A Formal Framework for Testing with Assertion Checkers in Mixed-Signal Simulation". To appear in Proc. IEEE International Conference on Electronics, Circuits, and Systems (ICECS'2012), Seville (Spain), December 2012.
[SIE12] L.PIERRE, L.FERRO, Z.BEL HADJ AMOR, P.BOURGON, J.QUEVREMONT: "Integrating PSL Properties into SystemC Transactional Modeling - Application to the Verification of a Modem SoC". Proc. IEEE International Symposium on Industrial Embedded Systems (SIES'2012), Karlsruhe (Germany), June 2012.
[NO12] G.TSILIGIANNIS, L.PIERRE: "A Mixed Verification Strategy Tailored for Networks on Chip". Proc. ACM/IEEE International Symposium on Networks-on-Chip, Lyngby (Denmark), May 2012.
[MB11] L.PIERRE, L.FERRO:
"Dynamic Verification of SystemC Transactional Models".
In "Model-Based Testing for Embedded Systems"
(Series "Computational Analysis, Synthesis, and Design of Dynamic Systems"), Chapter 22, CRC Press, September 2011.
CRC Press page
[FDL11] L.PIERRE, L.DAMRI: "Improvement of Assertion-Based Verification through the Generation of Proper Test Sequences". Proc. Forum on specification & Design Languages, Oldenburg (Germany), September 2011.
[FM11] L.FERRO, L.PIERRE, Z.BEL HADJ AMOR, J.LACHAIZE, V.LEFFTZ: "Runtime Verification of Typical Requirements for a Space Critical SoC Platform". Proc. 16th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'2011), Trento (Italy), August 2011, Springer LNCS 6959.
[IT11] R.CLAVEL, L.PIERRE, R.LEVEUGLE: "Towards Robustness Analysis using PVS". Proc. Conference on Interactive Theorem Proving (ITP'2011), Nijmegen (NL), August 2011, Springer LNCS 6898.
[LN10] L.FERRO, L.PIERRE: "ISIS: Runtime Verification of TLM Platforms". Design Methods from Modeling Languages for Embedded Systems and SoC's (Selected Contributions from FDL'09), Lecture Notes in Electrical Engineering, Springer, September 2010.
[MEM10] L.PIERRE, L.FERRO: "Enhancing the Assertion-Based Verification of TLM Designs with Reentrancy". Proc. ACM/IEEE International Conference on Formal Methods and Models for Codesign, Grenoble, July 2010.
[SIE10] V.LEFFTZ, J.BERTRAND, H.CASSE, C.CLIENTI, P.COUSSY, L.MAILLET-CONTOZ, P.MERCIER, P.MOREAU, L.PIERRE, E.VAUMORIN: "A Design Flow for Critical Embedded Systems". Proc. IEEE Symposium on Industrial Embedded Systems, Trento (Italy), July 2010.
[DDE10] A.HELMY, L.PIERRE, A.JANTSCH: "Theorem Proving Techniques for the Formal Verification of NoC Communications with Non-minimal Adaptive Routing". Proc. IEEE Symposium on Design and Diagnostics of Electronic Systems, Vienna (Austria), April 2010.
[DAT10] L.FERRO, L.PIERRE: "Formal Semantics for PSL Modeling Layer and Application to the Verification of Transactional Models". Proc. DATE'2010, Dresden (Germany), March 2010.
[DFT09] S.BAARIR, C.BRAUNSTEIN, R.CLAVEL, E.ENCRENAZ, J.M.ILIE,
R.LEVEUGLE, I.MOUNIER, L.PIERRE, D.POITRENAUD:
"Complementary Formal Approaches for Dependability Analysis".
Proc. IEEE International Symposium on Defect and Fault Tolerance in VLSI
Systems (DFT'09), Chicago (IL), October 2009.
IEEE page
[FDL09] L.FERRO, L.PIERRE: "ISIS: Runtime Verification of TLM Platforms". Proc. Forum on specification & Design Languages, Sophia Antipolis (France), September 2009.
[JES09] D.BORRIONE, A.HELMY, L.PIERRE,
J.SCHMALTZ: "A Formal Approach to the Verification of Networks on Chip".
EURASIP Journal on Embedded Systems, Vol. 2009.
Web page
[ACL09] L.PIERRE, R.CLAVEL, R.LEVEUGLE:
"ACL2 for the Verification of Fault-Tolerance Properties: First Results".
Proc. International Workshop On The ACL2 Theorem Prover and Its Applications,
Boston (MA), May 2009.
ACM page
[DDE09] F.OUCHET, D.BORRIONE, K.MORIN-ALLORY, L.PIERRE:
"High-level symbolic simulation for automatic model extraction".
Proc. IEEE Symposium on Design and Diagnostics of Electronic Systems,
Liberec (Czech Republic), April 2009.
IEEE page
[SEL09] R.LEVEUGLE, L.PIERRE, P.MAISTRI, R.CLAVEL: "Soft Error Effect and Register Criticality Evaluations: Past, Present and Future". Proc. IEEE Workshop on Silicon Errors in Logic - System Effects (SELSE), Stanford University (CA), March 2009.
[NOC09] D.BORRIONE, A.HELMY, L.PIERRE,
J.SCHMALTZ: Chapter "Formal Verification of Communications in Networks-on-Chips".
In Networks-on-Chips:
Theory and Practice, F.Gebali and H.Elmiligi editors, CRC Press
(Taylor and Francis group), 2009.
CRC Press page
[IDT08] L.FERRO, L.PIERRE, Y.LEDRU, L. DU BOUSQUET:
"Generation of Test Programs for the Assertion-Based Verification
of TLM Models". Proc. IEEE International Design and Test Workshop (IDT'08),
Monastir (Tunisia), December 2008.
IEEE page
[TC08] L.PIERRE, L.FERRO:
"A Tractable and Fast Method for Monitoring SystemC TLM
Specifications". IEEE Transactions on
Computers, Vol. 57(10), October 2008 (Special Section on Programming Models and Architectures
for Embedded Systems).
IEEE TC page
[SIC08] D.BORRIONE, A.HELMY, L.PIERRE,
J.SCHMALTZ: "Executable Formal Specification and Validation of NoC
Communication Infrastructures". Proc. 21st Symposium on Integrated
Circuits and Systems Design, Gramado (Brazil), September 2008. ACM.
ACM page
[NOC07] D.BORRIONE, A.HELMY, L.PIERRE,
J.SCHMALTZ: "A Generic Model for Formally Verifying NoC Communication
Architectures: A Case Study". Proc. ACM/IEEE International Symposium on
Networks-on-Chips (NOCS'2007), May 2007. IEEE Computer Society Press.
IEEE page
[SSM06] L.PIERRE: "Chapter 10 - VHDL".
In Software Specification Methods,
International Scientific and Technical Encyclopedia (ISBN 1905209347),
M.Frappier and H.Habrias Eds., 2006 (improvement of [SSM01]).
Web page
[SMACD06] D.BORRIONE, A.HELMY, L.PIERRE:
"ACL2-based Verification of the Communications in the Hermes Network on
Chip". Proc. International Workshop on Symbolic Methods and Applications
to Circuit Design (SMACD'06), October 2006.
pdf file
[AMAST04] M.CONTENSIN, L.PIERRE: "Model-Checking
Systems with Unbounded Variables without Abstraction". Proc.
10th International Conference on Algebraic Methodology and Software Technology
(AMAST'04), July 2004. LNCS 3116, Springer-Verlag.
Springer link
pdf file
[PPL03] E.GASCARD, L.PIERRE: "Formal
Proof of Applications Distributed in Symmetric Interconnection Networks".
Parallel Processing Letters
(PPL),
Volume 13 (1), March 2003.
Postscript file
[MEM03] M.CONTENSIN, L.PIERRE: "Combining
ACL2 and a ν-calculus Model-checker to Verify System-level Designs". Proc.
ACM & IEEE International Conference on Formal Methods and Models for Codesign
(MEMOCODE'03), June 2003. IEEE Computer Society Press.
IEEE proceedings
[FMPP02] E.GASCARD, L.PIERRE: "Mechanical
Verification of Hypercube Algorithms". Proc. International
Workshop "Formal Methods for Parallel Programming : Theory and
Applications"
(FMPPTA'02), Fort Lauderdale (FL), April 2002. IEEE Computer Society Press.
Postscript file
[SSM01] L.PIERRE: "VHDL: A Hardware Description Language and its simulation semantics". In Software Specification Methods: An Overview Using a Case Study, Springer-Verlag, FACIT series ("Formal Approaches to Computing and Information Technology"), M.Frappier and H.Habrias Eds., 2001.
[CHARME01] E.GASCARD, L.PIERRE:
"Induction-Oriented Formal Verification in Symmetric Interconnection
Networks".
In T.Margaria & T.Melham eds.,
Correct Hardware Design and Verification Methods,
LNCS 2144,
Springer-Verlag, 2001.
Postscript file
[JCSC00] L.PIERRE:
"Induction-Oriented Verification of Replicated Architectures Described in
VHDL". Journal of Circuits, Systems and Computers,
Volume 10 (3 & 4), 2000.
Abstract and pdf file
[TVLSI00] D.BORRIONE, J.DUSHINA, L.PIERRE:
"A Compositional Model for the Functional Verification of High-Level Synthesis Results". IEEE
Transactions on VLSI Systems, Volume 8 (5), October 2000.
Postscript file
Postscript file of a long version
[PDCS00] P.GEORGELIN, L.PIERRE, T.NGUYEN: "A Formal Approach for the Specification of Communications in Distributed Systems". Proc. 13th Int. Conference on Parallel and Distributed Computing Systems (PDCS'2000), Las Vegas, August 2000, ISCA (International Society for Computers and Their Applications).
[ICD98] D.BORRIONE, J.DUSHINA, L.PIERRE: "Formalization of Finite State Machines with Data Path for the Verification of High-Level Synthesis". Proc. IX Brazilian Symposium on Integrated Circuit Design, Rio de Janeiro, October 1998, IEEE Computer Society Press.
[Inv98] L.PIERRE: "Specification
of Communicating Processes in LOTOS
and in VHDL : a Case Study". Proc. International Workshop on
Specification
Techniques and Formal Methods (Invoicing'98), Nantes, March 1998.
Postscript file
[FTP97] E.GASCARD, L.PIERRE: "Two Approaches to the Formal Proof of Replicated Hardware Systems using the Boyer-Moore Theorem Prover". Proc. International Workshop on First Order Theorem Provers (FTP'97), Linz (Austria), October 1997.
[FMPP97] L.PIERRE: "VHDL Description, Boyer-Moore Specification and Formal Verification of a Parallel System for Finding a Maximum". Proc. Workshop "Formal Methods for Parallel Programming : Theory and Applications" (FMPPTA'97), Geneva, April 1997.
[EDTC96] L.PIERRE: "Formal
Specification of a Reactive System : an Exercise
in VHDL, LOTOS and UNITY". Proc. European Design & Test
Conference'96,
Paris, March 1996 (one page abstract).
pdf file
[CHA95] L.PIERRE: "Describing
and Verifying Synchronous Circuits with
the Boyer-Moore Theorem Prover". In P.Camurati & H.Eveking eds.,
Correct Hardware Design and Verification Methods, LNCS 987,
Springer-Verlag, 1995.
Postscript file
[TPCD94] L.PIERRE: "An
automatic generalization method for the inductive
proof of replicated and parallel architectures". In R.Kumar &
T.Kropf eds., Theorem Provers in Circuit Design, LNCS 901,
Springer-Verlag, 1995.
Postscript file
[EDAC94] F.NICOLI, L.PIERRE: "Formal
Verification of behavioural VHDL
specifications : a case study". Proc. Int. Conference EURO-DAC
with EURO-VHDL'94. Grenoble, September 1994. IEEE Computer Society
Press.
pdf file
M.ALLEMAND, F.NICOLI, L.PIERRE: "Formal Verification of Hardware using LP and Comparison with Nqthm". Proc. IASTED Internat. Conference on Applied Informatics. Annecy, May 1994.
[NATO93] D.BORRIONE, H.EVEKING, L.PIERRE: "Formal Proofs from HDL Descriptions". In Fundamentals and Standards in Hardware Description Languages, NATO ASI Series, Kluwer Academic Pub., 1993.
[CHDL93] L.PIERRE: "VHDL Description and Formal Verification of Systolic Multipliers". Proc. 11th Int. Symposium on CHDL and their Applications. Ottawa (Canada), April 1993. In D.Agnew & L.Claesen ed., Computer Hardware Description Languages and their Applications, North Holland, 1993.
[D&T92] D.BORRIONE, L.PIERRE, A.SALEM: "Formal Verification of VHDL Descriptions in the PREVAIL Environment". IEEE Design&Test Magazine, Vol.9 (2), June 1992.
[BPS92] D.BORRIONE, L.PIERRE, A.SALEM: "Formal Verification of VHDL Descriptions in Boyer-Moore : First Results". In VHDL for simulation, synthesis and formal proofs, Kluwer Academic Pub., 1992.
[CHDL91] L.PIERRE: "From a HDL Description to Formal Proof Systems : Principles and Mechanization". Proc. 10th International Symposium on CHDL and their Applications. Marseille, April 1991. In D.Borrione & R.Waxman ed., Computer Hardware Description Languages and their Applications, North Holland, 1991.
L.PIERRE: "One Aspect of Mechanizing Formal Proof of Hardware: the Generalization of Partial Specifications". Proc. ACM International Workshop on Formal Methods in VLSI Design. Miami (Fl), January 1991.
D.BORRIONE, L.PIERRE, A.SALEM: "Formal Verification of VHDL Descriptions in Boyer-Moore : First Results". Proc. First European Conference on VHDL Methods, Marseille. September 1990.
L.PIERRE: "The Formal Proof of Sequential Circuits described in CASCADE using the Boyer-Moore Theorem Prover". Proc. IFIP WG 10.2 Int. Workshop, November 1989. In L.Claesen ed., Formal VLSI Correctness Verification, North Holland 1990.
L.PIERRE: "The Formal Proof of the "Min-max" Sequential Benchmark described in CASCADE using the Boyer-Moore Theorem Prover". Proc. IFIP WG 10.2 Int. Workshop, November 1989. In L.Claesen ed., Formal VLSI Correctness Verification, North Holland 1990.
D.BORRIONE, J.L.PAILLET, L.PIERRE, H.COLLAVIZZA : "Modélisation fonctionnelle et preuve de circuits digitaux", T.S.I., Vol. 8, 6. December 1989 (in French).
D.BORRIONE, J.L.PAILLET, L.PIERRE: "Formal Verification of CASCADE descriptions". Proc. IFIP WG 10.2 International Working Conference on The Fusion of Hardware Design and Verification (Glasgow, July 1988), North Holland 1988.
Some internal
reports
[TIMA07] L.PIERRE: "A Model for
Assertion-Based Verification of TLM Designs".
TIMA Lab. Research Report TIMA-RR--07/09-01--FR, Grenoble, 2007.
PDF file
[LIM368] L.KLENOV, L.PIERRE: "Refinement
of Iterative Constructs in the B Method".
Rapport de Recherche LIM 368, Marseille, October
2001.
Postscript file
Here is the
Postscript file of the paper we presented at RCS'02 (International Workshop on Refinement of Critical Systems: Methods, Tools and Experience), Grenoble, January 2002
[RCS02].
[LIM338] E.GASCARD, L.PIERRE: "First
Steps toward the Mechanical
Verification of Distributed Programs in Symmetric Interconnection
Networks". Rapport de Recherche LIM 1999-338, Marseille, October
1999.
Postscript file
[LIM337] P.GEORGELIN, L.PIERRE, T.NGUYEN: "A Formal Specification of the MPI Primitives and Communication Mechanisms". Rapport de Recherche LIM 1999-337, Marseille, October 1999.
[LIM290] E.GASCARD, L.PIERRE:
"Généralisation de
théorèmes inductifs pour la vérification
d'architectures régulières". Rapport de Recherche
LIM 1998-290, Marseille, November 1998.
Postscript file
L.PIERRE, D.BORRIONE, J.DUSHINA: "Formalization of Finite State
Machines with Data Path". Internal Report TIMA, June 1998.
Extended version of the paper of Proc. IX Brazilian Symposium
on Integrated Circuit Design.
L.PIERRE: "A Comparative Evaluation of Different Formalisms for Specifying a Reactive System". Rapport de Recherche LIM 1995-137, Marseille, December 1995.
L.PIERRE: "Une introduction au démonstrateur de Boyer-Moore, Nqthm". Rapport de Recherche LIM 1995-109, Marseille, April 1995. (in French)