Bib fields

From FSL
Revision as of 16:48, 1 August 2013 by Stefane1 (Talk | contribs)

Jump to: navigation, search

Common fields (conference paper, journal paper, and technical report)

  • author: list of author names (possibly using LATEX code) as should appear in the bibliography of a paper when using "\cite"
  • title: must not contain LATEX code
  • abstract: must not contain LATEX code
  • project url (optional)
  • project name (optional)
  • author_id: "and" separated list of author names as should be used in "..." to link to the authors' homepage on FSL
  • category: comma (",") separated list of categories; each category must not contain whitespaces (it can contain "_" instead)
  • hidden (optional): by default drafts, submissions and technical reports are displayed only for logged in users, while publications are displayed for everybody; the hidden fields overrides this behavior
    • hidden = {false} papers are displayed for everybody
    • hidden = {true} papers are displayed only for logged-in users

Conference paper fields

  • both submission and publication
    • booktitle_acronym
    • booktitle_url
  • publication only (includes papers accepted but not published yet)
    • booktitle: conference name should not be abbreviated
    • publisher (optional): common values are ACM, IEEE, and Springer
    • series (optional): common values are LNCS, ENTCS
    • volume (optional)
    • month (optional): the month the conference takes place
    • year (optional): the year the conference takes place
    • pages (optional): should be completed after the paper is published
    • doi (optional): should be completed after the paper is published
    • presentation (optional): should be completed after the paper is presented

Journal paper fields

  • both submission and publication
    • journal_acronym
    • journal_url
  • publication only (includes papers accepted but not published yet)
    • journal: journal name should not be abbreviated
    • volume (optional)
    • number (optional)
    • pages (optional): should be completed after the paper is published
    • month (optional): the month the paper is published
    • year (optional): the year the paper is published
    • doi (optional): should be completed after the paper is published

Technical report fields

  • institution: institution name should not be abbreviated
  • month
  • year
  • number: typically the doi
  • doi (optional): if the number is the doi, the doi field may be omitted


Examples

Conference submission 

@inproceedings{rosu-stefanescu-2012-oopsla-submission,
  author    = {Grigore Rosu and Andrei Stefanescu},
  title     = {Checking Reachability using Matching Logic},
  abstract  = {
This paper presents a verification framework that is parametric in a (trusted)
operational semantics of some programming language.
The underlying proof system is language-independent and consists of eight proof
rules.
The proof system is proved partially correct and relatively complete (with
respect to the programming language configuration model).
To show its practicality, the generic framework is instantiated with a fragment
of C and evaluated with encouraging results.
  },

  author_id         = {Grigore Rosu and Andrei Stefanescu},
  category          = {fsl, executable_semantics, logics, matching_logic,
                       program_verification, programming_languages},
  project_url       = {http://matching-logic.org/},
  project_name      = {Matching Logic},
  booktitle_acronym = {OOPSLA'12},
  booktitle_url     = {http://splashcon.org/2012/cfp/378},
}

Conference publication 

@inproceedings{rosu-stefanescu-2012-oopsla,
  author    = {Grigore Ro\c{s}u and Andrei \c{S}tef\u{a}nescu},
  title     = {Checking Reachability using Matching Logic},
  abstract  = {
This paper presents a verification framework that is parametric in a (trusted)
operational semantics of some programming language.
The underlying proof system is language-independent and consists of eight proof
rules.
The proof system is proved partially correct and relatively complete (with
respect to the programming language configuration model).
To show its practicality, the generic framework is instantiated with a fragment
of C and evaluated with encouraging results.
  },
  booktitle = {Proceedings of the 27th Conference on Object-Oriented
               Programming, Systems, Languages, and Applications (OOPSLA'12)},
  pages     = {555-574},
  month     = {Oct},
  year      = {2012},
  publisher = {ACM},

  author_id         = {Grigore Rosu and Andrei Stefanescu},
  category          = {fsl, executable_semantics, logics, matching_logic,
                       program_verification, programming_languages},
  project_url       = {http://matching-logic.org},
  project_name      = {Matching Logic},
  booktitle_acronym = {OOPSLA'12},
  booktitle_url     = {http://splashcon.org/2012/cfp/378},
  doi               = {http://dl.acm.org/citation.cfm?doid=2384616.2384656},
  presentation      = {2012-10-24-rosu-stefanescu-OOPSLA},
}

Journal submission 

@article{endrullis-hendriks-bakhshi-rosu-2013-jfp-submission,
  author    = {J\"{o}rg Endrullis and Dimitri Hendriks and Rena Bakhshi and Grigore Ro\c{s}u},
  title     = {On the Complexity of Stream Equality},
  abstract  = {
We study the complexity of deciding the equality of streams specified
by systems of equations.
There are several notions of stream models in the literature, each
generating a different semantics of stream equality.
We pinpoint the complexity of each of these notions in the arithmetical
or analytical hierarchy.
Their complexity ranges from low levels of the arithmetical hierarchy
such as $\cpi{0}{2}$ for the most relaxed stream models, to
levels of the analytical hierarchy such as $\cpi{1}{1}$ and
up to subsuming the entire analytical hierarchy for more restricted but
natural stream models.
Since all these classes properly include both the semi-decidable
and co-semi-decidable classes, it follows that regardless of the
stream semantics employed, there is no complete proof system or algorithm
for determining equality or inequality of streams.
We also discuss several related problems, such as the existence and
uniqueness of stream solutions for systems of equations, as well as
the equality of such solutions.
  },
  journal           = {Journal of Functional Programming},
  year              = {2013},
  author_id         = {Joerg Endrullis and Dimitri Hendriks and Rena Bakhshi and Grigore Rosu},
  category          = {fsl, semantics, logics, programming_languages, behavioral_equivalence, circular_coinduction, automated_reasoning},
  project_url       = {http://fsl.cs.uiuc.edu/circ},
  project_name      = {CIRC},
  journal_acronym   = {JFP},
  journal_url       = {http://journals.cambridge.org/action/displayJournal?jid=JFP}
}

Journal publication 

@article{rosu-chen-2012-lmcs,
  author   = {Grigore Ro{\c s}u and Feng Chen},
  title    = {Semantics and Algorithms for Parametric Monitoring},
  abstract = {
Analysis of execution traces plays a fundamental role in many program
analysis approaches, such as runtime verification, testing, monitoring, and
specification mining. Execution traces are frequently parametric, i.e., they
contain events with parameter bindings. Each parametric trace usually
consists of many meaningful trace slices merged together, each slice
corresponding to one parameter binding. This gives a semantics-based
solution to parametric trace analysis. A general-purpose parametric trace
slicing technique is introduced, which takes each event in the parametric
trace and dispatches it to its corresponding trace slices. This parametric
trace slicing technique can be used in combination with any conventional,
non-parametric trace analysis technique, by applying the later on each
trace slice. As an instance, a parametric property monitoring technique is then
presented. The presented parametric trace slicing and monitoring techniques have
been implemented and extensively evaluated. Measurements of runtime
overhead confirm that the generality of the discussed techniques does not come
at a performance expense when compared with existing parametric trace
monitoring systems.
  },
  journal  = {Logical Methods in Computer Science},
  volume   = {8},
  number   = {1},
  pages    = {1-47},
  month    = {Feb},
  year     = {2012},
  note     = {Short version presented at TACAS 2009},

  author_id       = {Grigore Rosu and Feng Chen},
  category        = {fsl, javamop, logics, runtime_verification},
  journal_acronym = {J.LMCS},
  journal_url     = {http://www.lmcs-online.org/index.php},
  project_url     = {http://fsl.cs.uiuc.edu/index.php/MOP},
  project_name    = {MOP},
  doi             = {http://dx.doi.org/10.2168/LMCS-8(1:9)2012},
}

technical report 

@techreport{rosu-stefanescu-ciobaca-moore-2012-tr,
  author      = {Grigore Ro\c{s}u and Andrei \c{S}tef\u{a}nescu and \c{S}tefan
                 Ciob\^{a}c\u{a} and Brandon M. Moore},
  title       = {Reachability Logic},
  abstract    = {
This paper introduces *reachability logic*, a language-independent seven-rule
proof system for deriving reachability properties of systems.
The key ingredients of *reachability logic* are its sentences, which are called
*reachability rules* and generalize the transitions of operational semantics and
the Hoare triples of axiomatic semantics, and the *Circularity* proof rule,
which generalizes invariant proof rules for iterative and recursive constructs
in axiomatic semantics.
The target transition system is described as a set of reachability rules, which
are taken as axioms in a reachability logic proof.
Typical definition styles which can be read as collections of reachability rules
include conventional small-step and big-step operational semantics.
The reachability logic proof system is shown sound (in the sense of partial
correctness) and relatively complete.
The soundness result has also been formalized in Coq, allowing to convert
reachability logic proofs into proof certificates depending only on the
operational semantics and the unavoidable domain reasoning.
Reachability logic thus eliminates the need to independently define an axiomatic
and an operational semantics for each language, and the non-negligible effort to
prove the former sound and complete w.r.t the latter.
  },
  institution = {University of Illinois},
  month       = {Jul},
  year        = {2012},
  number      = {http://hdl.handle.net/2142/32952},

  author_id         = {Grigore Rosu and Andrei Stefanescu and Stefan Ciobaca and
                       Brandon Moore},
  category          = {fsl, executable_semantics, logics, matching_logic,
                       program_verification, programming_languages},
  project_url       = {http://fsl.cs.uiuc.edu/rl},
  project_name      = {Reachability Logic},
  hidden            = {false},
}
Retrieved from "http://fsl.cs.illinois.edu/index.php?title=Bib_fields&oldid=16625"
Personal tools
Namespaces

Variants
Actions
Navigation