
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
S.F. Siegel, G.S. Avrunin, "Improving the Precision of INCA by Eliminating Solutions with Spurious Cycles," IEEE Transactions on Software Engineering, vol. 28, no. 2, pp. 115128, February, 2002.  
BibTex  x  
@article{ 10.1109/32.988494, author = {S.F. Siegel and G.S. Avrunin}, title = {Improving the Precision of INCA by Eliminating Solutions with Spurious Cycles}, journal ={IEEE Transactions on Software Engineering}, volume = {28}, number = {2}, issn = {00985589}, year = {2002}, pages = {115128}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.988494}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Improving the Precision of INCA by Eliminating Solutions with Spurious Cycles IS  2 SN  00985589 SP115 EP128 EPD  115128 A1  S.F. Siegel, A1  G.S. Avrunin, PY  2002 KW  INCA KW  finitestate verification KW  cycles KW  integer programming. VL  28 JA  IEEE Transactions on Software Engineering ER   
The Inequality Necessary Condition Analyzer (INCA) is a finitestate verification tool that has been able to check properties of some very large concurrent systems. INCA checks a property of a concurrent system by generating a system of inequalities that must have integer solutions if the property can be violated. There may, however, be integer solutions to the inequalities that do not correspond to an execution violating the property. INCA thus accepts the possibility of an inconclusive result in exchange for greater tractability. We describe here a method for eliminating one of the two main sources of these inconclusive results.
[1] J.C. Corbett and G.S. Avrunin, "Using Integer Programming to Verify General Safety and Liveness Properties," Formal Methods in System Design, vol. 6, pp. 97123, Jan. 1995.
[2] Specification patterns web site.http://www.cis.ksu.edu/santosspecpatterns /. 2000.
[3] M.B. Dwyer, G.S. Avrunin, and J.C. Corbett, “Patterns in Property Specifications for FiniteState Verification,” Proc. 21st Int'l Conf. Software Eng., pp. 411–420, May 1999.
[4] G.S. Avrunin, J.C. Corbett, M.B. Dwyer, C.S. Pasareanu, and S.F. Siegel, ”Comparing FiniteState Verification Techniques for Concurrent Software,” Technical Report UMCS1999069, Dept. of Computer Science, Univ. of Massachusetts, Amherst, Nov. 1999.
[5] A.T. Chamillard, L.A. Clarke, and G.S. Avrunin, “An Empirical Comparison of Static Concurrency Analysis Techniques,” Technical Report 9684, Dept. of Computer Science, Univ. of Massachusetts, Amherst, 1996, revised, May 1997.
[6] J.C. Corbett, "An Empirical Evaluation of Three Methods for Deadlock Analysis of Ada Tasking Programs," Software Eng. Notes, pp. 204215, Proc. Int'l Symp. Software Testing and Analysis, Aug. 1994
[7] J.C. Corbett, “Evaluating Deadlock Detection Methods for Concurrent Software,” IEEE Trans. Software Eng., vol. 22, no. 3, pp. 161–179, Mar. 1996.
[8] G.J. Holzmann, “The Model Checker SPIN,” IEEE Trans. Software Eng., vol. 23, May 1997.
[9] K.L. McMillan, Symbolic Model Checking. Kluwer Academic, 1993.
[10] J.C. Corbett and G.S. Avrunin, "A Practical Method for Bounding the Time Between Events in Concurrent RealTime Systems," Proc. Int'l Symp. Software Testing and Analysis (ISSTA), Ostrand and Weyuker [37], New York: ACM Press, pp. 110116, June 1993.
[11] G.S. Avrunin, J.C. Corbett, L.K. Dillon, and J.C. Wileden, Automated Derivation of Time Bounds in Uniprocessor Concurrent Systems IEEE Trans. Software Eng., vol. 20, no. 9, 1994.
[12] J.C. Corbett and G.S. Avrunin, “Towards Scalable Compositional Analysis,” in Wile [26], pp. 53–61, Dec. 1994.
[13] K. Forester, C. MacFarlane, M. Cameron, and G. Bolcer, “Chiron1 User Manual,” Arcadia Document UCI9307, Univ. of California, Irvine, Sept. 1993.
[14] M.B. Dwyer and L.A. Clarke, "Data Flow Analysis for Verifying Properties of Concurrent Programs," Software Eng. Notes, vol. 19, no. 5, pp. 6275, Proc. ACM SIGSOFT Symp. Foundations of Software Eng., Dec. 1994.
[15] E.M. Clarke Jr., O. Grumberg, and D.A. Peled, Model Checking. MIT Press, 2000.
[16] Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems. SpringerVerlag, 1991.
[17] E.M. Clarke, E.A. Emerson, and A.P. Sistla, "Automatic verification of finitestate concurrent systems using temporal logic specifications," ACM Trans. Programming Languages and Systems, vol. 8, no. 2, pp. 244263, 1986.
[18] J.C. Corbett, M.B. Dwyer, J. Hatcliff, S. Laubach, C.S. Pasareanu, Robby, and H. Zheng, “Bandera: Extracting FiniteState Models from Java Source Code,” Proc. 22nd Int'l Conf. Software Eng., pp. 439–448, June 2000.
[19] M.B. Dwyer, J. Hatcliff, R. Joehanes, S. Laubach, C. Pasareanu, and H. Zheng, “ToolSupported Program Abstraction for FiniteState Verification,” Proc. 23rd Int'l Conf. Software Eng., pp. 177–187, May 2001.
[20] R.N. Taylor, “Complexity of Analyzing the Synchronization Structure of Concurrent Programs,” Acta Informatica, vol. 19, pp. 57–84, 1983.
[21] J. Reif and S. Smolka, “The Complexity of Reachability in Distributed Communicating Processes,” Acta Informatica, vol. 25, no. 3, pp. 333–354, 1988.
[22] R.H.B. Netzer and B.P. Miller, “On the Complexity of Event Ordering for SharedMemory Parallel Program Executions,” Proc. Int'l Conf. Parallel Processing, pp. II–93–II–97, Aug. 1990.
[23] T. Murata, “Petri Nets: Properties, Analysis and Application,” Proc. IEEE, vol. 77, no. 4, 1989.
[24] T. Murata, B. Shenker, and S.M. Shatz, "Detection of Ada Static Deadlocks Using Petri Net Invariants," IEEE Trans. Software Eng., vol. 15, no. 3, pp. 314326, Mar. 1989.
[25] J. Esparza and S. Melzer, “Verification of Safety Properties Using Integer Programming: Beyond the State Equation,” Formal Methods in System Design, vol. 16, pp. 159–189, 2000.
[26] D. Wile, ed., Proc. Second ACM SIGSOFT Symp. Foundations of Software Eng., Dec. 1994.