matthieu_moy.bib

@inproceedings{lussy,
  author = {Matthieu Moy and Florence Maraninchi and Laurent Maillet-Contoz},
  title = {{LusSy}: A Toolbox for the Analysis of Systems-on-a-Chip at the Transactional Level},
  booktitle = {International Conference on Application of Concurrency to System Design},
  year = 2005,
  month = {June},
  url = {http://www-verimag.imag.fr/~moy/publications/acsd05.pdf},
  pages = {26--35},
  abstract = {We describe a toolbox for the analysis of Systems-on-a-chip
  described in {SystemC} at the transactional level. The tools are able
  to extract information from {SystemC} code, and to build a set of
  parallel automata that capture the semantics of a {SystemC} design,
  including the transaction-level specific constructs. As far as we
  know, this provides the first executable formal semantics of
  {SystemC}. Being implemented as a traditional compiler front-end, it
  is able to deal with general {SystemC} designs. The intermediate
  representation is now connected to existing formal verification
  tools via appropriate encodings.  The toolbox is open and other
  tools will be used in the future.},
  note = {Acceptance rate: 23/45 = 51\%}
}
@inproceedings{pinapa,
  author = {Matthieu Moy and Florence Maraninchi and Laurent Maillet-Contoz},
  title = {{Pinapa}: An Extraction Tool for {SystemC} descriptions of Systems-on-a-Chip},
  booktitle = {EMSOFT},
  year = 2005,
  month = {September},
  url = {http://www-verimag.imag.fr/~moy/publications/sc-compil.pdf},
  code = {http://greensocs.sourceforge.net/pinapa/},
  pages = {317--324},
  abstract = {{SystemC} is becoming a de-facto standard for the description of
  complex systems-on-a-chip. It enables system-level descriptions of
  SoCs: the same language is used for the description of the
  architecture, software and hardware parts.
  
  A tool like pinapa is compulsory to work on realistic SoCs designs
  for anything else than simulation: it is able to extract both
  architecture and behavior information from {SystemC} code, with very
  few limitations. pinapa can be used as a front-end for various
  analysis tools, ranging from ``superlint'' to model-checking. It is
  open source and available from
  http://greensocs.sourceforge.net/pinapa/. There exists no equivalent
  tool for {SystemC} up to now.},
  note = {25/88 = 28\% accepted as regular papers, Rank A CORE 2014}
}
@incollection{tlm-book-chap5,
  author = {Matthieu Moy},
  title = {Chapter 5.9, Formal Verification},
  booktitle = {Transaction-Level Modeling with {SystemC}. {TLM} Concepts and Applications for Embedded Systems},
  pages = {190--206},
  publisher = {Springer},
  year = 2005,
  editor = {Frank Ghenassia},
  url = {http://www.springer.com/engineering/electronics/book/978-0-387-26232-1}
}
@article{lussy-journal,
  author = {Matthieu Moy and Florence Maraninchi and Laurent Maillet-Contoz},
  title = {{LusSy}: an open Tool for the Analysis of Systems-on-a-Chip at the Transaction Level},
  journal = {Design Automation for Embedded Systems},
  year = 2006,
  note = {special issue on {SystemC}-based systems},
  url = {http://www-verimag.imag.fr/~moy/publications/springer.pdf},
  abstract = {We describe a toolbox for the analysis of
                  Systems-on-a-chip written in {SystemC} at the
                  transaction level. The tool is able to extract
                  information from {SystemC} code, and to build a set of
                  parallel automata that capture the semantics of a
                  {SystemC} design, including the transaction-level
                  specific constructs. As far as we know, this
                  provides the first executable formal semantics of
                  {SystemC}. Being implemented as a traditional compiler
                  front-end, it is able to deal with general {SystemC}
                  designs. The intermediate representation is now
                  connected to existing formal verification tools via
                  appropriate encodings. The toolbox is open and other
                  tools will be used in the future.}
}
@online{framogr-software,
  author = {Matthieu Moy and V. H. Gupta and K. Gopinath},
  title = {{Framogr}: a {FRAMework} for the {MOdeling} and simulation of {GRoup} protocols},
  howpublished = {Published as Free Software (LGPL License)},
  year = 2006,
  note = {\url{http://download.gna.org/framogr/}}
}
@phdthesis{these-moy,
  author = {Matthieu Moy},
  title = {Techniques and Tools for the Verification of
                  Systems-on-a-Chip at the Transaction Level},
  school = {INPG, Grenoble, France},
  year = 2005,
  url = {http://www-verimag.imag.fr/~moy/phd/},
  month = {December},
  abstract = {  The work presented in this document deals with the formal
  verification models of Systems-on-a-Chip at the transaction level
  (TLM). We present the transaction level and its variants, and remind
  how this new level of abstraction is today necessary in addition to
  the register transfer level (RTL) to accommodate the growing
  constraints of productivity and quality, and how it integrates in
  the design flow.

  We present a new tool, called {LusSy}, that allows property-checking
  on transactional models written in {SystemC}. Its structure is similar
  to the one of a compiler: A front-end, {Pinapa}, that reads the
  source program, a semantic extractor, {Bise}, into our intermediate
  formalism {HPIOM}, a number of optimizations in the component {Birth},
  and code generators for provers like {Lustre} and {SMV}.

  {LusSy} has been designed to have as few limitation as possible
  regarding the way the input program is written. {Pinapa} uses a novel
  approach to extract the information from the {SystemC} program, and
  the semantic extraction implements several TLM constructs that have
  not been implemented in any other {SystemC} verification tool as of
  now. It doesn't require any manual annotation. The tool chain is
  completely automated.

  {LusSy} is currently able to prove properties on small platforms. Its
  components are reusable to build compositional verification tools,
  or static code analyzers using techniques other than model-checking
  that can scale up more efficiently.

  We present the theoretical principles for each step of the
  transformation, as well as our implementation. The results are given
  for small examples, and for a medium size case-study called EASY.
  Experimenting with {LusSy} allowed us to compare the various tools we
  used as provers, and to evaluate the effects of the optimizations we
  implemented.
}
}
@inproceedings{systemc-to-spin,
  author = {Claus Traulsen and J\'er\^ome Cornet and Matthieu Moy and Florence Maraninchi},
  title = {A {SystemC}/{TLM} semantics in {Promela} and its possible applications},
  booktitle = {14th Workshop on Model Checking Software SPIN},
  year = 2007,
  month = {July},
  url = {http://www-verimag.imag.fr/~moy/publications/MicMacToSpin.pdf},
  abstract = {{SystemC} has become a de-facto standard for the modeling of
systems-on-a-chip, at various levels of abstraction, including the
so-called transaction level (TL). Verifying properties of a TL model
requires that {SystemC} be translated into some formally defined
language for which there exist verification back-ends. Since {SystemC}
has no formal semantics, this includes a careful encoding of the
{SystemC} scheduler, which has both synchronous and asynchronous
features, and a notion of time. In a previous work, we described LusSy
a complete chain from {SystemC} to a synchronous formalism and its
associated verification tools. In this paper, we describe the encoding
of the {SystemC} scheduler into a asynchronous formalism, namely Promela
(the input language for {Spin}). We comment on the possible uses of
this new encoding, and compare it with the synchronous encoding.}
}
@article{helmstet:fmcad06,
  author = {Claude Helmstetter and Florence Maraninchi and Laurent Maillet-Contoz and Matthieu Moy},
  title = {Automatic Generation of Schedulings for Improving the Test Coverage of Systems-on-a-Chip},
  journal = {{FMCAD}},
  year = {2006},
  isbn = {0-7695-2707-8},
  pages = {171-178},
  doi = {http://doi.ieeecomputersociety.org/10.1109/FMCAD.2006.10},
  publisher = {IEEE Computer Society},
  address = {Los Alamitos, CA, USA},
  url = {http://www-verimag.imag.fr/~moy/publications/Helmstetter_FMCAD06.pdf},
  abstract = {{SystemC} is becoming a de-facto standard for the
early simulation of Systems-on-a-chip (SoCs). It is a parallel
language with a scheduler. Testing a SoC written in {SystemC}
implies that we execute it, for some well chosen data. We are
bound to use a particular deterministic implementation of the
scheduler, whose specification is non-deterministic. Consequently,
we may fail to discover bugs that would have appeared using
another valid implementation of the scheduler. Current methods
for testings SoCs concentrate on the generation of the inputs,
and do not address this problem at all. We assume that the
selection of relevant data is already done, and we generate
several schedulings allowed by the scheduler specification. We
use dynamic partial-order reduction techniques to avoid the
generation of two schedulings that have the same effect on
the system’s behavior. Exploring alternative schedulings during
testing is a way of guaranteeing that the SoC description, and
in particular the embedded software, is scheduler-independent,
hence more robust. The technique extends to the exploration of
other non-fully specified aspects of SoC descriptions, like timing.},
  note = {Acceptance rate: 21/90 = 23\%}
}
@inproceedings{MARANINCHI:2008:HAL-00311011:1,
  title = {{S}ystem{C}/{TLM} {S}emantics for {H}eterogeneous {S}ystem-on-{C}hip {V}alidation},
  author = {Maraninchi, Florence and Moy, Matthieu and Cornet, J{\'e}r{\^o}me and Maillet-Contoz, Laurent and Helmstetter, Claude and Traulsen, Claus},
  abstract = {{S}ystem{C} has become a de facto standard for the system-level description of systems-on-a-chip. {S}ystem{C}/{TLM} is a library dedicated to transaction level modeling. {I}t allows to define a virtual prototype of a hardware platform, on which the embedded software can be tested. {A}pplying formal validation techniques to {S}ystem{C} descriptions of {S}o{C}s requires that the semantics of the language be formalized. {T}he model of time and concurrency underlying the {S}ystem{C} definition is intermediate between pure synchrony and pure asynchrony. {W}e list the available solutions for the semantics of {S}ystem{C}/{TLM}, and explain how to connect {S}ystem{C} to existing formal validation tools.},
  keywords = {{S}ystem{C}; {TLM}; lustre; spin; promela; semantics; model-checking; verification; model; {S}o{C}; {S}ystem-on-a-{C}hip},
  language = {{A}nglais},
  affiliation = {{VERIMAG} - {IMAG} - {CNRS} : {UMR}5104 - {U}niversit{\'e} {J}oseph {F}ourier - {G}renoble {I} - {I}nstitut {N}ational {P}olytechnique de {G}renoble - {INPG} - {STM}icroelectronics ({G}renoble) - {ST}-{GRENOBLE} - {STM}icroelectronics - {STM}icroelectronics ({C}rolles) - {ST}-{CROLLES} - {STM}icroelectronics - {L}aboratoire {F}ranco-{C}hinois d'{I}nformatique, d'{A}utomatique et de {M}ath{\'e}matiques {A}ppliqu{\'e}es - {LIAMA} - {I}nstitute of {A}utomation, {C}hinese {A}cademy of {S}ciences - {C}hinese {A}cademy of {S}cience - {INRA} - {INRIA} - {BRGM} - {CIRAD} - {CNRS} - {FORMES} - {LIAMA} - {INRIA} - {T}singhua {U}niversity / {B}eijing - {LIAMA} - {I}nformatic {K}iel {U}niversity - {C}hristian-{A}lbrechts-{U}niversit{\"a}t, {K}iel },
  booktitle = {2008 {J}oint {IEEE}-{NEWCAS} and {TAISA} {C}onference 2008 {J}oint {IEEE}-{NEWCAS} and {TAISA} {C}onference },
  address = {{M}ontr{\'e}al {C}anada },
  editor = {{IEEE} },
  note = {{B}.6.3, {D}.2.4, {D}.3.1, {F}.4.3, {F}.3.1, {B}.8.1 },
  audience = {internationale },
  month = {June},
  year = {2008},
  url = {http://hal.archives-ouvertes.fr/hal-00311011/en/}
}
@inproceedings{besnard09:ssa-to-signal,
  author = {{B}esnard, {L}o{\"i}c and {G}autier, {T}hierry and {M}oy, Matthieu and {T}alpin, {J}ean-{P}ierre and {J}ohnson, {K}enneth and {M}araninchi, {F}lorence},
  title = {{A}utomatic translation of {C}/{C}++ parallel code into synchronous formalism using an {SSA} intermediate form},
  booktitle = {Ninth International Workshop on Automated Verification of Critical Systems (AVOCS'09)},
  year = 2009,
  month = {September},
  publisher = {Electronic Communications of the EASST},
  url = {http://www-verimag.imag.fr/~moy/publications/ssa-sig.pdf},
  abstract = {We present an approach for the translation of imperative code (like
  C, C++) into the synchronous formalism Signal, in order to use a
  model-checker to verify properties on the source code. The
  translation uses SSA as an intermediate formalism, and the GCC
  compiler as a front-end. The contributions of this paper with
  respect to previous work are a more efficient translation scheme,
  and the management of parallel code. It is applied successfully on
  simple {SystemC} examples.}
}
@inproceedings{causality-tacas2010,
  author = {Karine Altisen and Matthieu Moy},
  title = {Arrival Curves for Real-Time Calculus: the Causality Problem and its Solutions},
  booktitle = {TACAS},
  year = 2010,
  month = {March},
  pages = {358--372},
  editor = {J. Esparza and R. Majumdar},
  url = {http://www-verimag.imag.fr/~moy/publications/rtc-causality.pdf},
  abstract = {  The Real-Time Calculus (RTC) is a framework to analyze
  heterogeneous real-time systems that process event streams of data.
  The streams are characterized by pairs of curves, called arrival
  curves, that express upper and lower bounds on the number of events
  that may arrive over any specified time interval.
  System properties may then be computed using algebraic techniques in
  a compositional way.
  A well-known limitation of RTC is that it cannot model systems with
  states and recent works
  studied how to interface RTC curves with state-based models.
  Doing so, while trying, for example to generate a stream of events
  that satisfies some given pair of curves, we faced a
  causality problem: it can be the case
  that, once having generated a finite prefix of an event stream, the
  generator deadlocks, since no extension of the prefix can satisfy
  the curves anymore. When trying to express the property of the
  curves with state-based models, one may face the same problem.

  This paper formally defines the problem on arrival curves, and gives
  algebraic ways to characterize causal pairs of curves, i.e. curves
  for which the problem cannot occur.
  Then, we provide algorithms to compute a causal pair of curves
  equivalent to a given curve, in several models.  These algorithms
  provide a canonical representation for a pair of curves, which is
  the best pair of curves among the curves equivalent to the ones they
  take as input.  
},
  note = {Acceptance rate: 24/110 = 21\%, Rank A CORE 2014}
}
@inproceedings{rtc-ta-granularity,
  author = {Karine Altisen and Yanhong Liu and Matthieu Moy},
  title = {Performance Evaluation of Components Using a Granularity-based Interface Between Real-Time Calculus and Timed Automata},
  booktitle = {Eighth Workshop on Quantitative Aspects of Programming Languages (QAPL)},
  publisher = {Electronic Proceedings in Theoretical Computer Science},
  year = 2010,
  address = {Paphos, Cyprus},
  month = {March},
  url = {http://www-verimag.imag.fr/~moy/publications/gran-paper.pdf},
  abstract = {  To analyze complex and heterogeneous real-time embedded systems,
  recent works have proposed interface techniques between 
    real-time calculus (RTC) and timed automata (TA), in order
  to take advantage of the strengths of each technique for analyzing
  various components. But the time to analyze a state-based component
  modeled by TA may be prohibitively high, due to the state space
    explosion problem. In this paper, we propose a framework of
  granularity-based interfacing to speed up the analysis of a TA
  modeled component. First, we abstract fine models to work with
  event streams at coarse granularity. We perform analysis of the
  component at multiple coarse granularities and then based on RTC
  theory, we derive lower and upper bounds on arrival patterns of
  the fine output streams using the causality closure algorithm of
  \cite{causality-TACAS10}.  Our framework can help to achieve
  tradeoffs between precision and analysis time.}
}
@inproceedings{ac2lus,
  author = {Karine Altisen and Matthieu Moy},
  title = {ac2lus: Bringing {SMT}-solving and Abstract Interpretation Techniques to Real-Time Calculus through the Synchronous Language {Lustre}},
  booktitle = {22nd Euromicro Conference on Real-Time Systems (ECRTS)},
  year = 2010,
  address = {Brussels, Belgium},
  month = {July},
  abstract = {  We present an approach to connect the Real-Time Calculus (RTC)
  method to the synchronous data-flow language Lustre, and its
  associated tool-chain, allowing the use of techniques like
  SMT-solving and abstract interpretation which were not previously
  available for use with RTC.

  The approach is supported by a tool called ac2lus.
  It allows to model the system to be analyzed as general Lustre
  programs with inputs specified by arrival curves; the tool can
  compute output arrival curves or evaluate upper and lower bounds on
  any variable of the components, like buffer sizes.

  Compared to existing approaches to connect RTC to other formalisms,
  we believe that the use of Lustre, a real programming language, and
  the synchronous hypothesis make the task easier
  to write models, and we show that it allows a great flexibility of
  the tool itself, with many variants to fine-tune the performances.
},
  url = {http://www-verimag.imag.fr/~moy/publications/ac2lus-conf.pdf},
  note = {Acceptance rate: 27/112 = 24\%, Rank A CORE 2014}
}
@inproceedings{pinavm-emsoft,
  title = {{PinaVM}: a {SystemC} Front-End Based on an Executable Intermediate Representation},
  author = {Marquet, Kevin and Moy, Matthieu},
  abstract = {{SystemC} is the de facto standard for modeling
                  embedded systems. It allows system design at various
                  levels of ab- stractions, provides typical
                  object-orientation features and incorporates timing
                  and concurrency concepts. A {SystemC} program is
                  typically processed by a {SystemC} front-end in
                  order to verify, debug and/or optimize the
                  architecture. Designing a {SystemC} front-end is a
                  difficult task and existing approaches suffer from
                  limitations. In this paper, we present a new
                  approach that addresses most of these limitations.
                  We detail this approach, based on an executable
                  intermediate representation. We introduce
                  {PinaVM}, a new, open-source {SystemC} front-end
                  and implementation of our contributions. We give
                  experimental results on this tool.},
  keywords = {{M}odeling, {V}alidation, {S}ystem{C}, {S}ystem on {C}hip},
  language = {{A}nglais},
  affiliation = {{VERIMAG} - {IMAG} - {CNRS} : {UMR}5104 - {U}niversit{\'e} {J}oseph {F}ourier - {G}renoble {I} - {I}nstitut {N}ational {P}olytechnique de {G}renoble - {INPG} },
  booktitle = {International Conference on Embedded Software},
  pages = {79 },
  address = {{S}cottsdale, {USA}},
  collaboration = {{O}pen{TLM} },
  day = {24},
  month = {10},
  year = {2010},
  hal_id = {hal-00495874},
  url = {http://www-verimag.imag.fr/~moy/publications/pinavm-emsoft.pdf},
  note = {Acceptance rate: 29/89 = 32\%, Rank A CORE 2014}
}
@inproceedings{review-sc-fe,
  hal_id = {hal-00495886},
  title = {A Theoretical and Experimental Review of {SystemC} Front-ends},
  author = {Marquet, Kevin and Moy, Matthieu and Karkare, Bageshri},
  booktitle = {Forum for Design Languages (FDL)},
  abstract = {{SystemC} is a widely used tool for prototyping
                  {S}ystems-on-a-{C}hip. Being implemented as a
                  {C}++ library, a plain {C}++ compiler is sufficient
                  to compile and simulate a {SystemC} program.
                  However, a {SystemC} program needs to be
                  processed by a dedicated tool in order to visualize,
                  formally verify, debug and/or optimize the
                  architecture. In this paper we focus on the tools
                  (called front-ends) used in the initial stages of
                  processing {SystemC} programs. We describe the
                  challenges in developing {SystemC} front-ends and
                  present a survey of existing solutions. The
                  limitations and capabilities of these tools are
                  compared for various features of {SystemC} and
                  intended back-end applications. We present typical
                  examples that front-ends should ideally be able to
                  process, and give theoretical limitations as well as
                  experimental results of existing tools.},
  keywords = {{SystemC}, front-end, compilation, review},
  language = {{A}nglais},
  affiliation = {{VERIMAG} - {IMAG} - {CNRS} : {UMR}5104 - {U}niversit{\'e} {J}oseph {F}ourier - {G}renoble {I} - {I}nstitut {N}ational {P}olytechnique de {G}renoble - {INPG} },
  note = {{B}.1.4, {C}.3 {O}pen{TLM} ({P}rojet {M}inalogic) },
  collaboration = {{O}pen{TLM} },
  year = {2010},
  pdf = {http://www-verimag.imag.fr/~moy/publications/revue-sc-fe-fdl.pdf}
}
@inproceedings{MARQUET:2011:HAL-00557515:1,
  hal_id = {hal-00557515},
  url = {http://hal.archives-ouvertes.fr/hal-00557515/en/},
  title = { {E}fficient {E}ncoding of {S}ystem{C}/{TLM} in {P}romela},
  author = {Marquet, Kevin and Moy, Matthieu and Jeannet, Bertrand},
  abstract = {{T}o deal with the ever growing complexity of {S}ystems-on-{C}hip, designers use models early in the design flow. {S}ystem{C} is a commonly used tool to write such models. {I}n order to verify these models, one thriving approach is to encode its semantics into a formal language, and then to verify it with verification tools. {V}arious encodings of {S}ystem{C} into formal languages have already been proposed, with different performance implications. {I}n this paper, we investigate a new, automatic, asynchronous means to formalize models. {O}ur encoding supports the subset of the concurrency and communication constructs offered by {S}ystem{C} used for high-level modeling. {W}e increase the confidence in the fact that encoded programs have the same semantics as the original one by model-checking a set of properties. {W}e give experimental results on our formalization and compare with previous works.},
  keywords = {{S}ystem{C}, {T}ransaction-{L}evel {M}odeling, {P}romela, {S}pin, {M}odel-checking},
  booktitle = {{DATICS}-{IMECS}},
  address = {{H}ong-{K}ong },
  collaboration = {{P}rojet {M}inalogic {O}pen{TLM}},
  day = {16},
  month = {03},
  year = {2011},
  pdf = {http://www-verimag.imag.fr/~moy/publications/datics-imecs2011.pdf}
}
@inproceedings{FMMM-RAPIDO-11,
  title = {Faithfulness Considerations for Virtual Prototyping of Systems-on-Chip },
  author = {Funchal, Giovanni and Moy, Matthieu and Maillet-Contoz, Laurent and Maraninchi, Florence},
  month = {jan},
  year = {2011},
  booktitle = {3rd Workshop on: Rapid Simulation and Performance Evaluation: Methods and Tools (RAPIDO)},
  address = {Heraklion, Crete, Greece},
  team = {SYNC},
  abstract = {Virtual prototypes are simulators used in the consumer
                  electronics industry. They enable the development of
                  embedded software before the real, physical hardware
                  is available, hence providing important gains in
                  speed of development and time-to-market.
                  Transaction-level Modeling (TLM) is a widely used
                  technique for designing such virtual prototypes. Its
                  main insight is that many micro-architectural
                  details (i.e. caches, fifos and pipelines) can be
                  omitted from the model as they should not impact the
                  behavior perceived from a software programmer's
                  point-of-view. In this paper, we shall see that this
                  assumption is not always true, specially for
                  low-level software (e.g. drivers). As a result,
                  there may be bugs in the software which are not
                  observable on a TLM virtual prototype, designed
                  according to the current modeling practices. We call
                  this a "faithfulness" issue. Our experience shows
                  that many engineers are not aware of this issue.
                  Therefore, we provide an in-depth and intuitive
                  explanation of the sort of bugs that may be missed.
                  We claim that, to a certain extent, modified TLM
                  models can be faithful without losing the benefits
                  in terms of time-to-market and ease of modeling.
                  However, further investigation is required to
                  understand how this could be done in a more general
                  framework.},
  url = {http://www-verimag.imag.fr/~moy/publications/rapido2010.pdf}
}
@inproceedings{FunchalDATE2011,
  title = {{jTLM}: an Experimentation Framework for the Simulation of Transaction-Level Models of Systems-on-Chip},
  author = {Funchal, Giovanni and Moy, Matthieu},
  booktitle = {Design, Automation and Test in Europe (DATE)},
  url = {http://www-verimag.imag.fr/PUBLIS/uploads/aexel3895.pdf},
  team = {SYNC},
  year = {2011},
  abstract = {Virtual prototypes are simulators used in the consumer electronics industry. Transaction-level Modeling (TLM) is a widely used technique for designing such virtual prototypes. In particular, they allow for early development of embedded software.

The SystemC modeling language is the current industry standard for developing virtual prototypes. Our experience suggests that writing TLM models exclusively in SystemC leads sometimes to confusion between modeling concepts and their implementation, and may be the root of some known bad practices.

This paper introduces jTLM, an experimentation framework that allow us to study the extent to which common modeling issues come from a more fundamental constraint of the TLM approach. We focus on a discussion of the two modes of simulation scheduling: cooperative and preemptive. We confront the implications of these two modes on the way of designing TLM models, the software bugs exposed by the simulators and the performance. },
  note = {acceptance rate : 314/950 = 33\%, Rank A+ GDR SoC-SiP}
}
@online{pinavm-software,
  author = {Kevin Marquet and Matthieu Moy},
  title = {{PinaVM}: {P}ina{VM} {I}s {N}ot {A} {V}irtual {M}achine},
  howpublished = {Published as Free Software (LGPL License)},
  year = 2010,
  url = {https://forge.imag.fr/projects/pinavm/}
}
@online{pinapa-software,
  author = {Matthieu Moy},
  title = {{Pinapa}: {P}inapa {I}s {N}ot a {P}arser},
  howpublished = {Published as Free Software (LGPL License)},
  year = 2005,
  url = {http://greensocs.sourceforge.net/pinapa/}
}
@online{sc-during-software,
  author = {Matthieu Moy},
  title = {sc-during: tasks with duration for parallel programming in {SystemC}},
  howpublished = {Published as Free Software (LGPL License)},
  year = 2012,
  url = {https://forge.imag.fr/projects/sc-during/}
}
@techreport{VERIMAG-TR-2010-13,
  title = {Faithfulness Considerations for Virtual Prototyping of Systems-on-Chip},
  author = {Funchal, Giovanni and Moy, Matthieu and Maraninchi, Florence and Maillet-Contoz, Laurent},
  institution = {VERIMAG},
  url = {http://www-verimag.imag.fr/TR/TR-2010-13.pdf},
  team = {SYNC},
  year = {2010},
  abstract = {Virtual prototypes are simulators used in the consumer electronics industry. They enable the development of embedded software before the real, physical hardware is available, hence providing important gains in speed of development and time-to-market. Transaction-level Modeling (TLM) is a widely used technique for designing such virtual prototypes. Its main insight is that many micro-architectural details (i.e. caches, fifos and pipelines) can be omitted from the model as they should not impact the behavior perceived from a software programmer\'s point-of-view. In this paper, we shall see that this assumption is not always true, specially for low-level software (e.g. drivers). As a result, there may be bugs in the software which are not observable on a TLM virtual prototype, designed according to the current modeling practices. We call this a faithfulness issue. Our experience shows that many engineers are not aware of this issue. Therefore, we provide an in-depth and intuitive explanation of the sort of bugs that may be missed. We claim that, to a certain extent, modified TLM models can be faithful without losing the benefits in terms of time-to-market and ease of modeling. However, further investigation is required to understand how this could be done in a more general framework.\r\n }
}
@inproceedings{MOY:2011:HAL-00574783:1,
  hal_id = {hal-00574783},
  url = {http://hal.archives-ouvertes.fr/hal-00574783/en/},
  title = {{E}fficient and {P}layful {T}ools to {T}each {U}nix to {N}ew {S}tudents},
  author = {Moy, Matthieu},
  abstract = {{T}eaching {U}nix to new students is a common tasks in many higher schools. {T}his paper presents an approach to such course where the students progress autonomously with the help of the teacher. {T}he traditional textbook is complemented with a wiki, and the main thread of the course is a game, in the form of a treasure hunt. {T}he course finishes with a lab exam, where students have to perform practical manipulations similar to the ones performed during the treasure hunt. {T}he exam is graded fully automatically. {T}his paper discusses the motivations and advantages of the approach, and gives an overall view of the tools we developed. {T}he tools are available from the web, and open-source, hence re-usable outside the {E}nsimag.},
  keywords = {{U}nix, {E}ducation, {E}xam, {T}reasure {H}unt},
  language = {{A}nglais},
  affiliation = {{VERIMAG} - {IMAG} - {CNRS} : {UMR}5104 - {U}niversit{\'e} {J}oseph {F}ourier - {G}renoble {I} - {I}nstitut {N}ational {P}olytechnique de {G}renoble - {INPG} },
  booktitle = {16th {A}nnual {C}onference on {I}nnovation and {T}echnology in {C}omputer {S}cience {E}ducation {IT}i{CSE} },
  address = {{D}armstadt {A}llemagne },
  audience = {internationale },
  day = {27},
  month = {06},
  year = {2011},
  pdf = {http://hal.archives-ouvertes.fr/hal-00574783/PDF/unix-course.pdf},
  note = {Acceptance rate : 66/169 = 39\%, Rank A CORE 2014}
}
@inproceedings{FUNCHAL:2011:HAL-00595637:1,
  hal_id = {hal-00595637},
  url = {http://www-verimag.imag.fr/~moy/publications/jtlm-during.pdf},
  title = { Modeling of Time in Discrete-Event Simulation of Systems-on-Chip},
  author = {{F}unchal, {G}iovanni and Moy, Matthieu},
  abstract = {{T}oday's consumer electronics industry uses modeling and simulation to cope with the complexity and time-to-market challenges of designing high-tech devices. {I}n such context, {T}ransaction-{L}evel {M}odeling ({TLM}) is a widely spread modeling approach often used in conjunction with the {IEEE} standard {S}ystem{C} discrete-event simulator. {I}n this paper, we present a novel approach to modeling time that distinguishes between instantaneous actions and tasks with a duration. {W}e argue that this distinction should be natural to the user. {I}n addition, we show that it gives us important insight and better comprehension of what actions can overlap in time. {W}e are able to exploit this distinction to parallelize the simulation, achieving an important speedup and exposing subtle software bugs related to parallelism. {W}e propose a set of primitives and discuss the design decisions, expressiveness and semantics in depth. {W}e present a research simulator called j{TLM} that implements all these ideas.},
  keywords = {{TLM}, time, duration, {J}ava, {jTLM}},
  language = {{A}nglais},
  affiliation = {{VERIMAG} - {IMAG} - {CNRS} : {UMR}5104 - {U}niversit{\'e} {J}oseph {F}ourier - {G}renoble {I} - {I}nstitut {N}ational {P}olytechnique de {G}renoble - {INPG} - {STM}icroelectronics ({G}renoble) - {ST}-{GRENOBLE} - {STM}icroelectronics },
  booktitle = {{ACM}/{IEEE} {N}inth {I}nternational {C}onference on {F}ormal {M}ethods and {M}odels for {C}odesign {MEMOCODE} },
  address = {{C}ambridge {R}oyaume-{U}ni },
  audience = {internationale },
  collaboration = {{HELP} },
  day = {11},
  month = {07},
  year = {2011},
  note = {Acceptance rate : 16/43 = 37\%}
}
@inproceedings{ALTISEN:2011:HAL-00648628:1,
  author = {Karine Altisen and Matthieu Moy},
  hal_id = {hal-00648628},
  url = {http://www-verimag.imag.fr/~moy/publications/wctt2011.pdf},
  title = {Causality closure for a new class of curves in real-time calculus},
  abstract = {{Real-Time Calculus (RTC) is a framework to analyze heterogeneous real-time systems that process event streams of data. The streams are characterized by arrival curves which express upper and lower bounds on the number of events that may arrive over any specified time interval. System properties may then be computed using algebraic techniques in a compositional way. The property of causality on arrival curves essentially characterizes the absence of deadlock in the corresponding generator. A mathematical operation called causality closure transforms arbitrary curves into causal ones. In this paper, we extend the existing theory on causality to the class Upac of infinite curves represented by a finite set of points plus piecewise affine functions, where existing algorithms did not apply. We show how to apply the causality closure on this class of curves, prove that this causal representative is still in the class and give algorithms to compute it. This provides the tightest pair of curves among the curves which accept the same sets of streams.}},
  keywords = {algorithms, causality, real-time calculus},
  language = {Anglais},
  affiliation = {Verimag - IMAG},
  booktitle = {{Proceedings of the 1st International Workshop on Worst-Case Traversal Time}},
  publisher = {ACM},
  pages = {3--10},
  address = {Vienna, Autriche},
  audience = {internationale},
  doi = {10.1145/2071589.2071590 },
  year = {2011},
  pdf = {http://hal.archives-ouvertes.fr/hal-00648628/PDF/wctt2011-final.pdf}
}
@online{unix-training-software,
  author = {Matthieu Moy},
  title = {Unix-training: a set of tools to teach {U}nix efficiently},
  howpublished = {Published as Free Software (LGPL License)},
  year = 2011,
  url = {http://www-verimag.imag.fr/~moy/?Unix-training-a-set-of-tools-to}
}
@online{chamilotools-software,
  author = {Matthieu Moy and S\'ebastien Viardot},
  title = {Chamilotools: a set of tools to interact with a Chamilo server},
  howpublished = {Published as Free Software (CeciLL C License)},
  year = 2016,
  url = {https://gitlab.com/chamilotools/chamilotools}
}
@inproceedings{Henry_Monniaux_Moy_SAS2012,
  title = {Succinct Representations for Abstract Interpretation},
  author = {Henry, Julien and Monniaux, David and Moy, Matthieu},
  booktitle = {Static analysis Symposium (SAS)},
  team = {SYNC},
  year = {2012},
  note = {Acceptance rate: 40\%, Rank A CORE 2014}
}
@online{pagai-software,
  author = {Julien Henry and David Monniaux and Matthieu Moy},
  title = {{PAGAI} static analyzer: Path Analysis for invariant Generation by Abstract Interpretation},
  howpublished = {Published as Free Software (CECILL-C License)},
  year = 2011,
  url = {https://forge.imag.fr/projects/pagai/}
}
@online{libtlmpwt-software,
  author = {Claude Helmstetter and Matthieu Moy},
  title = {{LIBTLMPWT}: Model Power-Consumption and Temperature in SystemC/TLM},
  howpublished = {Published as Free Software (GPL License)},
  year = 2013,
  url = {http://www-verimag.imag.fr/~moy/?LIBTLMPWT-Model-Power-Consumption}
}
@inproceedings{Henry_Monniaux_Moy_TAPAS2012,
  title = {{PAGAI}: a path sensitive static analyzer},
  author = {Henry, Julien and Monniaux, David and Moy, Matthieu},
  editor = {Bertrand Jeannet},
  booktitle = {Tools for Automatic Program Analysis (TAPAS)},
  team = {SYNC},
  year = {2012},
  abstract = {We describe the design and the implementation of PAGAI, a new static analyzer working over the LLVM compiler infrastructure, which computes inductive invariants on the numerical variables of the analyzed program. PAGAI implements various state-of-the-art algorithms combining abstract interpretation and decision procedures (SMT-solving), focusing on distinction of paths inside the control flow graph while avoiding systematic exponential enumerations. It is parametric in the abstract domain in use, the iteration algorithm, and the decision procedure. We compared the time and precision of various combinations of analysis algorithms and abstract domains, with extensive experiments both on personal benchmarks and widely available GNU programs.}
}
@inproceedings{cornet:hal-00716051,
  title = {{Co-Simulation of a SystemC TLM Virtual Platform with a Power Simulator at the Architectural Level: Case of a Set-Top Box}},
  author = {Cornet, J\'er\^ome and Maillet-Contoz, Laurent and Materic, Ilija and Kaiser, Sylvian and Boussetta, Hela and Bouhadiba, Tayeb and Moy, Matthieu and Maraninchi, Florence},
  booktitle = {{Design Automation Conference}},
  address = {San Francisco, US},
  month = {June},
  pages = {SESSION 10U: USER TRACK},
  url = {http://hal.archives-ouvertes.fr/hal-00716051},
  team = {SYNC},
  year = {2012},
  hal_id = {hal-00716051},
  keywords = {power estimation; temperature; systemc; transaction-level modeling},
  language = {Anglais},
  affiliation = {STMicroelectronics (Grenoble) - ST-GRENOBLE , Docea Power , VERIMAG - VERIMAG - IMAG},
  audience = {internationale},
  abstract = {{The ability to perform power estimation early in the design flow is becoming more and more critical as power optimization requirements grow. For now, standalone power simulators allow such estimation, based on typical stimuli described in a use-case scenario. We propose a co-simulation of SystemC TLM platforms with a Power model. This way, the Power model benefits from more realistic stimuli. In addition, it is possible to provide real-time information from the Power model back to the SystemC TLM simulation, such as temperature values.}}
}
@inproceedings{moy:hal-00761047,
  hal_id = {hal-00761047},
  url = {http://hal.archives-ouvertes.fr/hal-00761047},
  title = {{Parallel Programming with SystemC for Loosely Timed Models: A Non-Intrusive Approach}},
  author = {Moy, Matthieu},
  abstract = {{The SystemC/TLM technologies are widely accepted in the industry for fast system-level simulation. An important limitation of SystemC regarding performance is that the reference implementation is sequential, and the official semantics makes parallel executions difficult. As the number of cores in computers increase quickly, the ability to take advantage of the host parallelism during a simulation is becoming a major concern. Most existing work on parallelization of SystemC targets cycle-accurate simulation, and would be inefficient on loosely timed systems since they cannot run in parallel processes that do not execute simultaneously. We propose an approach that explicitly targets loosely timed systems, and offers the user a set of primitives to express tasks with duration, as opposed to the notion of time in SystemC which allows only instantaneous computations and time elapses without computation. Our tool exploits this notion of duration to run the simulation in parallel. It runs on top of any (unmodified) SystemC implementation, which lets legacy SystemC code continue running as-it-is. This allows the user to focus on the performance-critical parts of the program that need to be parallelized.}},
  keywords = {SystemC; TLM; parallelism; multi-core; loosely-timed},
  language = {Anglais},
  affiliation = {VERIMAG - VERIMAG - IMAG},
  booktitle = {{The Design, Automation, and Test in Europe (DATE)}},
  address = {Grenoble, France},
  audience = {internationale },
  year = {2013},
  month = mar,
  pdf = {http://www-verimag.imag.fr/~moy/IMG/pdf/sc-during.pdf},
  note = {16.4\% accepted as long-paper, Rank A+ GDR SoC-SiP}
}
@inproceedings{bmm-date-13,
  title = {System-Level Modeling of Energy in {TLM} for Early Validation of Power and Thermal Management},
  author = {Bouhadiba, Tayeb and Moy, Matthieu and Maraninchi, Florence},
  booktitle = {Design Automation and Test Europe (DATE)},
  address = {Grenoble, France},
  month = mar,
  team = {SYNC},
  url = {http://hal.archives-ouvertes.fr/hal-00807048},
  pdf = {http://www-verimag.imag.fr/~moy/publications/granu-date2013.pdf},
  year = {2013},
  note = {16.4\% accepted as long-paper, Rank A+ GDR SoC-SiP}
}
@inproceedings{helmstetter:hal-00807046,
  title = {{Fast and Accurate TLM Simulations using Temporal Decoupling for FIFO-based Communications}},
  author = {Helmstetter, Claude and Cornet, J\'er\^ome and Galil\'ee, Bruno and Moy, Matthieu and VIVET, Pascal},
  booktitle = {{Design, Automation and Test in Europe (DATE)}},
  address = {Grenoble, France},
  month = {Mar},
  pages = {1185},
  url = {http://hal.archives-ouvertes.fr/hal-00807046},
  team = {SYNC},
  year = {2013},
  hal_id = {hal-00807046},
  language = {Anglais},
  affiliation = {Laboratoire d'Electronique et des Technologies de l'Information - LETI , STMicroelectronics (Grenoble) - ST-GRENOBLE , VERIMAG - IMAG},
  audience = {internationale},
  pdf = {http://hal.archives-ouvertes.fr/hal-00807046/PDF/TDpaper.pdf},
  abstract = {{Untimed models of large embedded systems, generally written using SystemC/TLM, allow the software team to start simulations before the RTL description is available, and then provide a golden reference model to the verification team. For those two purposes, only a correct functional behavior is required, but users are asking more and more for timing estimations early in the design flow. Because companies cannot afford to maintain two simulators for the same chip, only local modifications of the untimed model are considered. A known approach is to add timing annotations into the code and to reduce the number of costly context switches using temporal decoupling, meaning that a process can go ahead of the simulation time before synchronizing again. Our current goal is to apply temporal decoupling to the TLM platform of a many-core SoC dedicated to high performance computing. Part of this SoC communicates using classic memory-mapped buses, but it can be extended with hardware accelerators communicating using FIFOs. Whereas temporal decoupling for memory-based transactions has been widely studied, FIFO-based communications raise issues that have not been addressed before. In this paper, we provide an efficient solution to combine temporal decoupling and FIFO-based communications.}},
  note = {acceptance rate: 302/829 = 36.4\% all categories, Rank A+ GDR SoC-SiP}
}
@inproceedings{bouhadiba:hal-00807354,
  hal_id = {hal-00807354},
  url = {http://hal.archives-ouvertes.fr/hal-00807354},
  title = {{Co-Simulation of Functional SystemC TLM Models with Power/Thermal Solvers}},
  author = {Bouhadiba, Tayeb and Moy, Matthieu and Maraninchi, Florence and Cornet, J{\'e}r{\^o}me and Maillet-Contoz, Laurent and Materic, Ilija},
  abstract = {{Modern systems-on-chips need sophisticated power-management policies to control their power consumption and temperature. These power-management policies are usually implemented partly in software, with hardware support. They need to be validated early, hence power and temperature-aware simulation techniques at the system-level need to be developed. Existing approaches for system-level power and thermal analysis usually either completely abstract the functionality (allowing only simple scenarios to be simulated), or run the functional simulation independently from the non-functional one. The approach presented in this paper allows a coupled simulation of a SystemC/TLM model, possibly including the actual embedded software, with a power and temperature solver such as ATMI or the commercial tool ACEplorer. Power and temperature analysis is done based on the stimuli sent by the SystemC/TLM platform, which in turn can take decisions based on the non-functional simulation.}},
  language = {Anglais},
  affiliation = {VERIMAG - IMAG , STMicroelectronics (Grenoble), Docea Power},
  booktitle = {{Virtual Prototyping of Parallel and Embedded Systems (VIPES)}},
  address = {Boston, US},
  audience = {internationale },
  year = {2013},
  month = may,
  pdf = {http://hal.archives-ouvertes.fr/hal-00807354/PDF/vipes2013.pdf}
}
@article{moy:hal-00986536,
  hal_id = {hal-00986536},
  url = {http://hal.archives-ouvertes.fr/hal-00986536},
  title = {{Compte-rendu d'habilitation : Mod{\'e}lisation {\`a} haut niveau d'abstraction pour les syst{\`e}mes embarqu{\'e}s}},
  author = {Moy, Matthieu},
  abstract = {{Les syst{\`e}mes embarqu{\'e}s modernes ont atteint
                  un niveau de complexit{\'e} qui fait qu'il n'est
                  plus possible d'attendre les premiers prototypes
                  physiques pour valider les d{\'e}cisions sur
                  l'int{\'e}gration des composants mat{\'e}riels et
                  logiciels. Il est donc n{\'e}cessaire d'utiliser des
                  mod{\`e}les, t{\^o}t dans le flot de conception. Les
                  travaux pr{\'e}sent{\'e}s dans ce document
                  contribuent {\`a} l'{\'e}tat de l'art dans plusieurs
                  domaines. Nous pr{\'e}sentons dans un premier temps
                  de nouvelles techniques de v{\'e}rification de
                  programmes {\'e}crits dans des langages
                  g{\'e}n{\'e}ralistes comme C, C++ ou Java. Dans un
                  second temps, nous utilisons des outils de
                  v{\'e}rification formelle sur des mod{\`e}les
                  {\'e}crits en SystemC au niveau transaction (TLM).
                  Plusieurs approches sont pr{\'e}sent{\'e}es, la
                  plupart d'entre elles utilisent des techniques de
                  compilations sp{\'e}cifiques {\`a} SystemC pour
                  transformer le programme SystemC en un format
                  utilisable par les outils. La seconde partie du
                  document s'int{\'e}resse aux propri{\'e}t{\'e}s
                  non-fonctionnelles des mod{\`e}les : performances
                  temporelles, consommation {\'e}lectrique et
                  temp{\'e}rature. Dans le contexte de la
                  mod{\'e}lisation TLM, nous proposons plusieurs
                  techniques pour enrichir des mod{\`e}les
                  fonctionnels avec des informations
                  non-fonctionnelles. Enfin, nous pr{\'e}sentons les
                  contributions faites {\`a} l'analyse de performance
                  modulaire (MPA) avec le calcul temps-r{\'e}el (RTC).
                  Nous proposons plusieurs connections entre ces
                  mod{\`e}les analytiques et des formalismes plus
                  expressifs comme les automates temporis{\'e}s et le
                  langage de programmation Lustre. Ces connexion
                  posent le probl{\`e}me th{\'e}orique de la
                  causalit{\'e}, qui est formellement d{\'e}fini et
                  r{\'e}solu avec un algorithme nouveau dit de "
                  fermeture causale ".}},
  language = {French},
  affiliation = {VERIMAG - IMAG},
  pages = {285-293},
  journal = {Technique et Science Informatiques},
  volume = {33},
  number = {3},
  year = {2014},
  pdf = {http://hal.archives-ouvertes.fr/hal-00986536/PDF/hdr-matthieu-moy-fr.pdf}
}
@phdthesis{hdr-moy,
  title = { High-level Models for Embedded Systems },
  author = {Moy, Matthieu},
  year = {2014},
  month = {March},
  address = {Verimag},
  type = {Habilitation \`a Diriger des Recherches ({HDR})},
  school = {{Univ. Grenoble Alpes, F-38000 Grenoble, France}},
  team = {SYNC},
  url = {http://www-verimag.imag.fr/~moy/?Habilitation-a-Diriger-des},
  pdf = {http://www-verimag.imag.fr/~moy/IMG/pdf/hdr-matthieu-moy.pdf}
}
@inproceedings{rihani:hal-01243244,
  title = {{WCET analysis in shared resources real-time systems with TDMA buses}},
  author = {Rihani, Hamza and Moy, Matthieu and Maiza, Claire and Altmeyer, Sebastian},
  url = {https://hal.archives-ouvertes.fr/hal-01243244},
  booktitle = {{RTNS 2015}},
  address = {Lille, France},
  series = {23rd International Conference on Real-Time Networks and Systems},
  year = {2015},
  month = nov,
  doi = {10.1145/2834848.2834871},
  keywords = {wcet ;  tdma ;  worst-case execution time ;  bus ;  multi-core ;  smt},
  pdf = {http://www-verimag.imag.fr/~moy/publications/rtns-2015.pdf},
  hal_id = {hal-01243244},
  hal_version = {v1},
  team = {SYNC}
}
@inproceedings{challenges-2015-rsp,
  title = {{Challenges for the Parallelization of Loosely Timed SystemC Programs}},
  author = {Becker, Denis and Moy, Matthieu and Cornet, J\'er\^ome},
  booktitle = {IEEE International Symposium on Rapid System Prototyping (RSP)},
  url = {https://hal.archives-ouvertes.fr/hal-01214891},
  pdf = {http://www-verimag.imag.fr/~moy/publications/rsp-2015.pdf},
  team = {SYNC},
  year = {2015}
}
@inproceedings{sycview-2016-duhde,
  title = {{SycView: Visualize and Profile SystemC Simulations}},
  author = {Becker, Denis and Cornet, J\'er\^ome and Moy, Matthieu},
  booktitle = {{DUHDe}},
  address = {Dresden, Germany},
  month = {Mar},
  series = {3rd Workshop on Design Automation for Understanding Hardware Designs},
  url = {https://hal.archives-ouvertes.fr/hal-01243265},
  pdf = {http://www-verimag.imag.fr/~moy/publications/duhde2016.pdf},
  team = {SYNC},
  year = {2016},
  hal_id = {hal-01243265},
  hal_version = {v1}
}
@article{moy:hal-01339441,
  title = {{Modeling Power Consumption and Temperature in TLM Models}},
  author = {Moy, Matthieu and Helmstetter, Claude and Bouhadiba, Tayeb and Maraninchi, Florence},
  url = {https://hal.archives-ouvertes.fr/hal-01339441},
  journal = {{Leibniz Transactions on Embedded Systems}},
  publisher = {{European Design and Automation Association (EDAA) \ EMbedded Systems Special Interest Group (EMSIG) and Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik GmbH, Dagstuhl Publishing.}},
  volume = {Vol 3},
  number = {No 1},
  pages = {03:1-03:29},
  year = {2016},
  month = jun,
  doi = {10.4230/LITES-v003-i001-a003},
  keywords = {Systemc ; Tlm ; Energy ; atmi},
  pdf = {http://www-verimag.imag.fr/~moy/publications/63-285-3-PB.pdf},
  hal_id = {hal-01339441},
  hal_version = {v1}
}
@inproceedings{RMM16,
  title = {{Efficient Execution of Dependent Tasks on Many-Core Processors}},
  author = {Rihani, Hamza and Maiza, Claire and Moy, Matthieu},
  booktitle = {{RTSOPS 2016}},
  address = {Toulouse, France},
  month = {Jul},
  series = {7th International Real-Time Scheduling Open Problems Seminar},
  team = {SYNC},
  year = {2016},
  keywords = {WCRT Analysis; Shared Resource Interference; Dependent Tasks; Synchronous Data flow; Many-cores; Scheduling},
  pdf = {http://www-verimag.imag.fr/~moy/publications/rtsops2016.pdf},
  url = {https://hal.archives-ouvertes.fr/view/index/docid/1406057}
}
@inproceedings{RMMDA16,
  title = {{Response Time Analysis of Synchronous Data Flow Programs on a Many-Core Processor}},
  author = {Rihani, Hamza and Moy, Matthieu and Maiza, Claire and Davis, Robert I. and Altmeyer, Sebastian},
  booktitle = {{RTNS 2016}},
  address = {Brest, France},
  month = {Oct},
  series = {24th International Conference on Real-Time Networks and Systems},
  team = {SYNC},
  year = {2016},
  doi = {10.1145/2997465.2997472},
  keywords = {WCRT Analysis; Shared Resource Interference; Dependent Tasks; Synchronous Data flow; Many-cores; Scheduling},
  url = {https://hal.archives-ouvertes.fr/view/index/docid/1406145},
  pdf = {http://www-verimag.imag.fr/~moy/publications/rtns16-conf.pdf}
}
@article{rtc-fmsd16,
  title = {Causality Problem in Real-Time Calculus},
  author = {Altisen, Karine and Moy, Matthieu},
  journal = {Formal Methods in System Design (Springer)},
  number = {1},
  pages = {1--45},
  url = {https://hal.archives-ouvertes.fr/view/index/docid/1406162},
  volume = {48},
  team = {SYNC},
  year = {2016},
  doi = {10.1007/s10703-016-0250-y},
  issn = {1572-8102},
  pdf = {http://www-verimag.imag.fr/~moy/publications/causality-springer.pdf},
  note = {Rank A CORE ERA2010}
}
@article{parallel-syc-2016-electronics,
  title = {{Parallel Simulation of Loosely Timed SystemC/TLM Programs: Challenges Raised by an Industrial Case Study}},
  author = {Becker, Denis and Moy, Matthieu and Cornet, J\'er\^ome},
  editor = {Fr\'ed\'eric Rousseau and Gabriela Nicolescu and Amer Baghdadi and Mostafa Bassiouni},
  journal = {MDPI Electronics},
  number = {2},
  pages = {22},
  url = {https://hal.archives-ouvertes.fr/hal-01321055},
  volume = {5},
  team = {SYNC},
  year = {2016},
  doi = {10.3390/electronics5020022},
  pdf = {http://www-verimag.imag.fr/~moy/publications/electronics-05-00022.pdf},
  issn = {2079-9292}
}

This file was generated by bibtex2html 1.98.