Changeset 3444


Ignore:
Timestamp:
Feb 17, 2014, 12:37:33 PM (6 years ago)
Author:
mulligan
Message:

More language changes. At end of file.

Location:
Papers/fopara2013
Files:
2 edited

Legend:

Unmodified
Added
Removed

  • Papers/fopara2013/fopara13.bib

    r3443 r3444  
    292292  key = {cerco}
    293293}
     294
     295@misc
     296{ jessie,
     297  url = {http://krakatoa.lri.fr/},
     298  title = {Jessie {Frama-C} plugin},
     299  key = {jessie}
     300}

  • Papers/fopara2013/fopara13.tex

    r3443 r3444  
    931931
    932932Not all the details of the non-functional state needs to be exposed, and the
    933 technique works better when the part of state that is required can be summarized
     933technique works better when the part of state that is required can be summarised
    934934in a simple data structure. For example, to handle simple but realistic
    935935pipelines it is sufficient to remember a short integer that encodes the position
    … …  
    957957same technique works for loop unrolling without modification: the function will
    958958assign one cost to the even iterations and another cost to the odd
    959 ones.  The loop optimisation code
    960 that duplicate the loop bodies must also modify the code to correctly propagate
     959ones.  The optimisation code
     960that duplicates the loop bodies must also modify the code to correctly propagate
    961961the update of the iteration numbers. The technical details are more complicated and
    962962can be found in the CerCo reports and publications. The implementation, however,
    … …  
    993993Frama-C \cite{framac} is a set of analysers for C programs with a
    994994specification language called ACSL. New analyses can be dynamically added
    995 via a plugin system. For instance, the Jessie plugin allows deductive
     995via a plugin system. For instance, the Jessie plugin~\cite{jessie} allows deductive
    996996verification of C programs with respect to their specification in ACSL, with
    997997various provers as back-end tools.
    … …  
    10241024analysis of the VCs associated with branching may lead to a complexity blow up.
    10251025
    1026 \paragraph{Experience with Lustre.} Lustre is a data-flow language for programming
     1026\paragraph{Experience with Lustre.} Lustre~\cite{lustre} is a data-flow language for programming
    10271027synchronous systems, with a compiler which targets C. We designed a
    10281028wrapper for supporting Lustre files.
    … …  
    10601060loop in the logic assertions. This logic function takes the variant as a first
    10611061parameter. The other parameters of $f$ are the free variables of the body of the
    1062 loop. An axiom is added to account the fact that the cost is accumulated at each
     1062loop. An axiom is added to account for the fact that the cost is accumulated at each
    10631063step of the loop.
    10641064The cost of the function is directly added as post-condition of the function.
    … …  
    10941094\section{Conclusions and future work}
    10951095
    1096 All the CerCo software and deliverables can be found on the CerCo homepage at~\url{http://cerco.cs.unibo.it}.
     1096All CerCo software and deliverables may be found on the project homepage~\cite{cerco}.
    10971097
    10981098The results obtained so far are encouraging and provide evidence that
    … …  
    11081108architecture that admits a cost model that is execution history independent.
    11091109The most important future work is dealing with hardware architectures
    1110 characterized by history dependent stateful components, like caches and
     1110characterised by history-dependent stateful components, like caches and
    11111111pipelines. The main issue is to assign a parametric, dependent cost
    11121112to basic blocks that can be later transferred by the labelling approach to
Note: See TracChangeset for help on using the changeset viewer.