@article{CabalarFandinoGareaetal.2020,
  author    = {Cabalar, Pedro and Fandi{\~n}o, Jorge and Garea, Javier and Romero, Javier and Schaub, Torsten},
  title     = {Eclingo},
  series = {Theory and practice of logic programming},
  volume    = {20},
  journal   = {Theory and practice of logic programming},
  number    = {6},
  publisher = {Cambridge Univ. Press},
  address   = {New York},
  issn      = {1471-0684},
  doi       = {10.1017/S1471068420000228},
  pages     = {834 -- 847},
  year      = {2020},
  abstract  = {We describe eclingo, a solver for epistemic logic programs under Gelfond 1991 semantics built upon the Answer Set Programming system clingo. The input language of eclingo uses the syntax extension capabilities of clingo to define subjective literals that, as usual in epistemic logic programs, allow for checking the truth of a regular literal in all or in some of the answer sets of a program. The eclingo solving process follows a guess and check strategy. It first generates potential truth values for subjective literals and, in a second step, it checks the obtained result with respect to the cautious and brave consequences of the program. This process is implemented using the multi-shot functionalities of clingo. We have also implemented some optimisations, aiming at reducing the search space and, therefore, increasing eclingo 's efficiency in some scenarios. Finally, we compare the efficiency of eclingo with two state-of-the-art solvers for epistemic logic programs on a pair of benchmark scenarios and show that eclingo generally outperforms their obtained results.},
  language  = {en}
}
@article{FandinoLifschitzLuehneetal.2020,
  author    = {Fandi{\~n}o, Jorge and Lifschitz, Vladimir and L{\"u}hne, Patrick and Schaub, Torsten},
  title     = {Verifying tight logic programs with Anthem and Vampire},
  series = {Theory and practice of logic programming},
  volume    = {20},
  journal   = {Theory and practice of logic programming},
  number    = {5},
  publisher = {Cambridge Univ. Press},
  address   = {Cambridge [u.a.]},
  issn      = {1471-0684},
  doi       = {10.1017/S1471068420000344},
  pages     = {735 -- 750},
  year      = {2020},
  abstract  = {This paper continues the line of research aimed at investigating the relationship between logic programs and first-order theories. We extend the definition of program completion to programs with input and output in a subset of the input language of the ASP grounder gringo, study the relationship between stable models and completion in this context, and describe preliminary experiments with the use of two software tools, anthem and vampire, for verifying the correctness of programs with input and output. Proofs of theorems are based on a lemma that relates the semantics of programs studied in this paper to stable models of first-order formulas.},
  language  = {en}
}
@article{KuentzerKrstić2020,
  author    = {Kuentzer, Felipe A. and Krstić, Miloš},
  title     = {Soft error detection and correction architecture for asynchronous bundled data designs},
  series = {IEEE transactions on circuits and systems},
  volume    = {67},
  journal   = {IEEE transactions on circuits and systems},
  number    = {12},
  publisher = {Institute of Electrical and Electronics Engineers},
  address   = {New York},
  issn      = {1549-8328},
  doi       = {10.1109/TCSI.2020.2998911},
  pages     = {4883 -- 4894},
  year      = {2020},
  abstract  = {In this paper, an asynchronous design for soft error detection and correction in combinational and sequential circuits is presented. The proposed architecture is called Asynchronous Full Error Detection and Correction (AFEDC). A custom design flow with integrated commercial EDA tools generates the AFEDC using the asynchronous bundled-data design style. The AFEDC relies on an Error Detection Circuit (EDC) for protecting the combinational logic and fault-tolerant latches for protecting the sequential logic. The EDC can be implemented using different detection methods. For this work, two boundary variants are considered, the Full Duplication with Comparison (FDC) and the Partial Duplication with Parity Prediction (PDPP). The AFEDC architecture can handle single events and timing faults of arbitrarily long duration as well as the synchronous FEDC, but additionally can address known metastability issues of the FEDC and other similar synchronous architectures and provide a more practical solution for handling the error recovery process. Two case studies are developed, a carry look-ahead adder and a pipelined non-restoring array divider. Results show that the AFEDC provides equivalent fault coverage when compared to the FEDC while reducing area, ranging from 9.6\% to 17.6\%, and increasing energy efficiency, which can be up to 6.5\%.},
  language  = {en}
}