# Bib fields

From FSL

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
- presentations should be added to SVN under presentations/YYYY (year). Use the filename of the presentation without extension (extensions are inferred; automatically adds all versions if multiple files are present, e.g., pdf and ppt).
- Note that keynote presentations are actually directories, so you need to archive them and name the archive *.key. E.g., for foo.key do: $ mv foo.key bar.key; zip -r foo.key bar.key

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}, }

@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}, }