Work on the bibliography

2 files changed, 20 insertions, 2 deletions

diff --git a/lsr_env.tex b/lsr_env.tex
index 188ebe4..371f8ca 100644
--- a/lsr_env.tex
+++ b/lsr_env.tex
@@ -27,7 +27,7 @@
 % Layout
 % ==========================================================================
 \setuppapersize[A4][A4]
-\definefontfeature	[default][default][protrusion=quality,expansion=quality]
+\definefontfeature[default][default][protrusion=quality,expansion=quality]
 \setupalign[hz,hanging,lesshyphenation,verytolerant]
 \setupbodyfont[ebgaramondlato,11pt]
 %\setupalign[hz,hanging,nothyphenated]
diff --git a/lsr_refs.bib b/lsr_refs.bib
index 2d4720c..4ac943b 100644
--- a/lsr_refs.bib
+++ b/lsr_refs.bib
@@ -10,7 +10,6 @@
 	url = {https://doi.org/10.1109/IEEESTD.2005.339572},
 	ISSN = {},
 	key = {IEEE Std 1364.1},
-	keywords = {IEC Standards;Verilog;Registers},
 	month = {},
 	type = {Standard}
 }
@@ -65,6 +64,7 @@
 }
 
 @article{barthe14_formal_verif_ssa_based_middl_end_compc,
+	year = {2014},
 	abstract = {CompCert is a formally verified compiler that generates compact and efficient code for a large subset of the C language. However, CompCert foregoes using SSA, an intermediate representation employed by many compilers that enables writing simpler, faster optimizers. In fact, it has remained an open problem to verify formally an SSA-based compiler. We report on a formally verified, SSA-based middle-end for CompCert. In addition to providing a formally verified SSA-based middle-end, we address two problems raised by Leroy in [2009]: giving an intuitive formal semantics to SSA, and leveraging its global properties to reason locally about program optimizations.},
 	author = {Barthe, Gilles and Demange, Delphine and Pichardie, David},
 	location = {New York, NY, USA},
@@ -278,6 +278,20 @@
 	url = {https://doi.org/10.1145/775832.775928}
 }
 
+@inproceedings{cong06_sdc,
+	year = {2006},
+	abstract = {Scheduling plays a central role in the behavioral synthesis process, which automatically compiles high-level specifications into optimized hardware implementations. However, most of the existing behavior-level scheduling heuristics either have a limited efficiency in a specific class of applications or lack general support of various design constraints. In this paper we describe a new scheduler that converts a rich set of scheduling constraints into a system of difference constraints (SDC) and performs a variety of powerful optimizations under a unified mathematical programming framework. In particular, we show that our SDC-based scheduling algorithm can efficiently support resource constraints, frequency constraints, latency constraints, and relative timing constraints, and effectively optimize longest path latency, expected overall latency, and the slack distribution. Experiments demonstrate that our proposed technique provides efficient solutions for a broader range of applications with higher quality of results (in terms of system performance) when compared to the state-of-the-art scheduling heuristics},
+	author = {Cong, J. and Zhiru Zhang},
+	url = {https://doi.org/10.1145/1146909.1147025},
+	booktitle = {2006 43rd ACM/IEEE Design Automation Conference},
+	date = {2006-07},
+	doi = {10.1145/1146909.1147025},
+	issn = {0738-100X},
+	keywords = {high-level synthesis,static scheduling},
+	pages = {433--438},
+	title = {An efficient and versatile scheduling algorithm based on SDC formulation}
+}
+
 @article{cong11_high_level_synth_fpgas,
 	author = {Jason Cong and
                Bin Liu and
@@ -970,6 +984,7 @@ and Morawiec, Adam",
 }
 
 @inproceedings{ottenstein90_progr_depen_web,
+	year = {1990},
 	abstract = {The Program Dependence Web (PDW) is a program representation that can be directly interpreted using control-, data-, or demand-driven models of execution. A PDW combines a single-assignment version of the program with explicit operators that manage the flow of data values. The PDW can be viewed as an augmented Program Dependence Graph. Translation to the PDW representation provides the basis for projects to compile Fortran onto dynamic dataflow architectures and simulators. A second application of the PDW is the construction of various compositional semantics for program dependence graphs.},
 	author = {Ottenstein, Karl J. and Ballance, Robert A. and MacCabe, Arthur B.},
 	location = {White Plains, New York, USA},
@@ -1050,6 +1065,7 @@ and Morawiec, Adam",
 }
 
 @inproceedings{pilato13_bambu,
+	year = {2013},
 	author = {{Pilato}, C. and {Ferrandi}, F.},
 	booktitle = {2013 23rd International Conference on Field programmable Logic and Applications},
 	date = {2013},
@@ -1140,6 +1156,7 @@ and Morawiec, Adam",
 }
 
 @article{six20_certif_effic_instr_sched,
+	year = {2020},
 	abstract = {CompCert is a moderately optimizing C compiler with a formal, machine-checked, proof of correctness: after successful compilation, the assembly code has a behavior faithful to the source code. Previously, it only supported target instruction sets with sequential semantics, and did not attempt reordering instructions for optimization. We present here a CompCert backend for a VLIW core (i.e. with explicit parallelism at the instruction level), the first CompCert backend providing scalable and efficient instruction scheduling. Furthermore, its highly modular implementation can be easily adapted to other VLIW or non-VLIW pipelined processors.},
 	author = {Six, Cyril and Boulmé, Sylvain and Monniaux, David},
 	location = {New York, NY, USA},
@@ -1155,6 +1172,7 @@ and Morawiec, Adam",
 }
 
 @unpublished{six21_verif_super_sched_relat_optim,
+	year = {2021},
 	author = {Six, Cyril and Gourdin, Léo and Boulmé, Sylvain and Monniaux, David},
 	url = {https://hal.archives-ouvertes.fr/hal-03200774},
 	date = {2021-04},