How about formal verification?# CS - 计算机科学
m*n
1 楼
Is it promising or not?
Is it practically feasible?
What is its application?
Thx.
Is it practically feasible?
What is its application?
Thx.
c*e
2 楼
大家可以讨论一下，.这个和testing 相比那个将来更好一些.
formal verification paper不少.不知道工业界的情况.Combinational equivalence
checking没什么作的八.
sequential的太难,没什么突破.很多人发BMC方面的东西，好像这个工业界开始用了。微
软好像对于软件的
verification很感兴趣，有不少人在做 software verification.
【在 m****n 的大作中提到】
: Is it promising or not?
: Is it practically feasible?
: What is its application?
: Thx.
formal verification paper不少.不知道工业界的情况.Combinational equivalence
checking没什么作的八.
sequential的太难,没什么突破.很多人发BMC方面的东西，好像这个工业界开始用了。微
软好像对于软件的
verification很感兴趣，有不少人在做 software verification.
【在 m****n 的大作中提到】
: Is it promising or not?
: Is it practically feasible?
: What is its application?
: Thx.
h*n
3 楼
PCC? proof carry code?
微
【在 c****e 的大作中提到】
: 大家可以讨论一下，.这个和testing 相比那个将来更好一些.
: formal verification paper不少.不知道工业界的情况.Combinational equivalence
: checking没什么作的八.
: sequential的太难,没什么突破.很多人发BMC方面的东西，好像这个工业界开始用了。微
: 软好像对于软件的
: verification很感兴趣，有不少人在做 software verification.
微
【在 c****e 的大作中提到】
: 大家可以讨论一下，.这个和testing 相比那个将来更好一些.
: formal verification paper不少.不知道工业界的情况.Combinational equivalence
: checking没什么作的八.
: sequential的太难,没什么突破.很多人发BMC方面的东西，好像这个工业界开始用了。微
: 软好像对于软件的
: verification很感兴趣，有不少人在做 software verification.
w*g
4 楼
Proof carrying code generates publications but is it practical?
【在 h****n 的大作中提到】
: PCC? proof carry code?
:
: 微
【在 h****n 的大作中提到】
: PCC? proof carry code?
:
: 微
R*r
5 楼
type annotations are proofs, too...
【在 w*******g 的大作中提到】
: Proof carrying code generates publications but is it practical?
【在 w*******g 的大作中提到】
: Proof carrying code generates publications but is it practical?
T*r
6 楼
I feel "The Source is the Proof" by Vivek Handar et. al from UC Irvine
is more practical. PCC is good in theory, though.
【在 w*******g 的大作中提到】
: Proof carrying code generates publications but is it practical?
is more practical. PCC is good in theory, though.
【在 w*******g 的大作中提到】
: Proof carrying code generates publications but is it practical?
v*t
7 楼
Software testing is also very promising. The top PhD graduate in software
engineering this year is working on software testing. See
http://www.cs.washington.edu/homes/taoxie/
As somebody already mentioned, he maintains software engineering genealogy.
I have heard different people from different schools said he is the top
candidate in software engineering this year.
I know another Indian student who just graduated in Feb. He went to Microsoft
Research, Redmond. He is also working on software test
【在 c****e 的大作中提到】
: 大家可以讨论一下，.这个和testing 相比那个将来更好一些.
: formal verification paper不少.不知道工业界的情况.Combinational equivalence
: checking没什么作的八.
: sequential的太难,没什么突破.很多人发BMC方面的东西，好像这个工业界开始用了。微
: 软好像对于软件的
: verification很感兴趣，有不少人在做 software verification.
engineering this year is working on software testing. See
http://www.cs.washington.edu/homes/taoxie/
As somebody already mentioned, he maintains software engineering genealogy.
I have heard different people from different schools said he is the top
candidate in software engineering this year.
I know another Indian student who just graduated in Feb. He went to Microsoft
Research, Redmond. He is also working on software test
【在 c****e 的大作中提到】
: 大家可以讨论一下，.这个和testing 相比那个将来更好一些.
: formal verification paper不少.不知道工业界的情况.Combinational equivalence
: checking没什么作的八.
: sequential的太难,没什么突破.很多人发BMC方面的东西，好像这个工业界开始用了。微
: 软好像对于软件的
: verification很感兴趣，有不少人在做 software verification.
r*y
8 楼
do you think SE is a very promising direction in CS field. I guess it is not!
It seems that the current promising directions for finding CS faculty jobs are
"security, sensor network, system, and theory". maybe more?
Microsoft
。
【在 v*****t 的大作中提到】
: Software testing is also very promising. The top PhD graduate in software
: engineering this year is working on software testing. See
: http://www.cs.washington.edu/homes/taoxie/
: As somebody already mentioned, he maintains software engineering genealogy.
: I have heard different people from different schools said he is the top
: candidate in software engineering this year.
: I know another Indian student who just graduated in Feb. He went to Microsoft
: Research, Redmond. He is also working on software test
It seems that the current promising directions for finding CS faculty jobs are
"security, sensor network, system, and theory". maybe more?
Microsoft
。
【在 v*****t 的大作中提到】
: Software testing is also very promising. The top PhD graduate in software
: engineering this year is working on software testing. See
: http://www.cs.washington.edu/homes/taoxie/
: As somebody already mentioned, he maintains software engineering genealogy.
: I have heard different people from different schools said he is the top
: candidate in software engineering this year.
: I know another Indian student who just graduated in Feb. He went to Microsoft
: Research, Redmond. He is also working on software test
w*g
9 楼
if you are real good, any field can be a promising field.
【在 r*****y 的大作中提到】
: do you think SE is a very promising direction in CS field. I guess it is not!
: It seems that the current promising directions for finding CS faculty jobs are
: "security, sensor network, system, and theory". maybe more?
:
: Microsoft
: 。
【在 r*****y 的大作中提到】
: do you think SE is a very promising direction in CS field. I guess it is not!
: It seems that the current promising directions for finding CS faculty jobs are
: "security, sensor network, system, and theory". maybe more?
:
: Microsoft
: 。
r*y
10 楼
well, not really.
Some fields in CS are almost dead. no funding opportunity, and the stuff make
no much sense for industry either. No many deparment like to hire new faculty
in this kind of directions.
not!
are
software
genealogy.
【在 w*******g 的大作中提到】
: if you are real good, any field can be a promising field.
Some fields in CS are almost dead. no funding opportunity, and the stuff make
no much sense for industry either. No many deparment like to hire new faculty
in this kind of directions.
not!
are
software
genealogy.
【在 w*******g 的大作中提到】
: if you are real good, any field can be a promising field.
w*g
11 楼
if you put this way, an able guy may do well in fields like security,
real-time, prog lang, db, embedded system, AI, networking, algorithm,
bioinfo, software engr, ... almost every fields I can think of.
any cold field out there in CS?
【在 r*****y 的大作中提到】
: well, not really.
: Some fields in CS are almost dead. no funding opportunity, and the stuff make
: no much sense for industry either. No many deparment like to hire new faculty
: in this kind of directions.
:
: not!
: are
: software
: genealogy.
real-time, prog lang, db, embedded system, AI, networking, algorithm,
bioinfo, software engr, ... almost every fields I can think of.
any cold field out there in CS?
【在 r*****y 的大作中提到】
: well, not really.
: Some fields in CS are almost dead. no funding opportunity, and the stuff make
: no much sense for industry either. No many deparment like to hire new faculty
: in this kind of directions.
:
: not!
: are
: software
: genealogy.
x*g
12 楼
security and bioinformatics are hot in faculty job market. not sure about
other fields.
not!
are
genealogy.
equivalence
了
【在 r*****y 的大作中提到】
: do you think SE is a very promising direction in CS field. I guess it is not!
: It seems that the current promising directions for finding CS faculty jobs are
: "security, sensor network, system, and theory". maybe more?
:
: Microsoft
: 。
other fields.
not!
are
genealogy.
equivalence
了
【在 r*****y 的大作中提到】
: do you think SE is a very promising direction in CS field. I guess it is not!
: It seems that the current promising directions for finding CS faculty jobs are
: "security, sensor network, system, and theory". maybe more?
:
: Microsoft
: 。
v*t
13 楼
SE may be not as hot as "securit, sensor network, system, and theory", but the
job market demand is still there. I am also working on SE and plan to graduate
soon. From what I saw on ACM/IEEE/CRA job postings, there are a lot of
departments that are hiring in the SE area.
Some people said if you work on formal methods, you're dead and will not be
able to find a job in the academia. I am afraid I cannot agree with this
point, either. As far as I know, formal methods are very much appreciated in
t
【在 r*****y 的大作中提到】
: do you think SE is a very promising direction in CS field. I guess it is not!
: It seems that the current promising directions for finding CS faculty jobs are
: "security, sensor network, system, and theory". maybe more?
:
: Microsoft
: 。
job market demand is still there. I am also working on SE and plan to graduate
soon. From what I saw on ACM/IEEE/CRA job postings, there are a lot of
departments that are hiring in the SE area.
Some people said if you work on formal methods, you're dead and will not be
able to find a job in the academia. I am afraid I cannot agree with this
point, either. As far as I know, formal methods are very much appreciated in
t
【在 r*****y 的大作中提到】
: do you think SE is a very promising direction in CS field. I guess it is not!
: It seems that the current promising directions for finding CS faculty jobs are
: "security, sensor network, system, and theory". maybe more?
:
: Microsoft
: 。
x*r
14 楼
Hardware verification seems to be quite promising.
You can use it in chip design
【在 m****n 的大作中提到】
: Is it promising or not?
: Is it practically feasible?
: What is its application?
: Thx.
You can use it in chip design
【在 m****n 的大作中提到】
: Is it promising or not?
: Is it practically feasible?
: What is its application?
: Thx.
T*r
15 楼
cannot agree more. formal method is always a good thing in academia. it is
computer *science*, not computer *engineering*. the more I get into it, the
more I appreciate it.
【在 v*****t 的大作中提到】
: SE may be not as hot as "securit, sensor network, system, and theory", but the
: job market demand is still there. I am also working on SE and plan to graduate
: soon. From what I saw on ACM/IEEE/CRA job postings, there are a lot of
: departments that are hiring in the SE area.
: Some people said if you work on formal methods, you're dead and will not be
: able to find a job in the academia. I am afraid I cannot agree with this
: point, either. As far as I know, formal methods are very much appreciated in
: t
computer *science*, not computer *engineering*. the more I get into it, the
more I appreciate it.
【在 v*****t 的大作中提到】
: SE may be not as hot as "securit, sensor network, system, and theory", but the
: job market demand is still there. I am also working on SE and plan to graduate
: soon. From what I saw on ACM/IEEE/CRA job postings, there are a lot of
: departments that are hiring in the SE area.
: Some people said if you work on formal methods, you're dead and will not be
: able to find a job in the academia. I am afraid I cannot agree with this
: point, either. As far as I know, formal methods are very much appreciated in
: t
w*g
16 楼
but many computer scientists are really engineering.
【在 T********r 的大作中提到】
: cannot agree more. formal method is always a good thing in academia. it is
: computer *science*, not computer *engineering*. the more I get into it, the
: more I appreciate it.
【在 T********r 的大作中提到】
: cannot agree more. formal method is always a good thing in academia. it is
: computer *science*, not computer *engineering*. the more I get into it, the
: more I appreciate it.
h*t
17 楼
解释一下名词吧。 什么是combinational equivalence checking?
什么是BMC，为什么sequential 太难 ？
【在 c****e 的大作中提到】
: 大家可以讨论一下，.这个和testing 相比那个将来更好一些.
: formal verification paper不少.不知道工业界的情况.Combinational equivalence
: checking没什么作的八.
: sequential的太难,没什么突破.很多人发BMC方面的东西，好像这个工业界开始用了。微
: 软好像对于软件的
: verification很感兴趣，有不少人在做 software verification.
什么是BMC，为什么sequential 太难 ？
【在 c****e 的大作中提到】
: 大家可以讨论一下，.这个和testing 相比那个将来更好一些.
: formal verification paper不少.不知道工业界的情况.Combinational equivalence
: checking没什么作的八.
: sequential的太难,没什么突破.很多人发BMC方面的东西，好像这个工业界开始用了。微
: 软好像对于软件的
: verification很感兴趣，有不少人在做 software verification.
h*t
18 楼
would that be type checking, instead of model checking?
【在 R****r 的大作中提到】
: type annotations are proofs, too...
【在 R****r 的大作中提到】
: type annotations are proofs, too...
h*t
19 楼
BMC is bounded model checking. 记得有一篇很新的paper 说BMC是decidable.
【在 h****t 的大作中提到】
: 解释一下名词吧。 什么是combinational equivalence checking?
: 什么是BMC，为什么sequential 太难 ？
【在 h****t 的大作中提到】
: 解释一下名词吧。 什么是combinational equivalence checking?
: 什么是BMC，为什么sequential 太难 ？
m*n
20 楼
好象欧洲比米国做的好,那儿的大牛不少.
好多牛VERIFICATION的会议在欧洲开.
搞的俺PAPER没少发,会一个没参加.
DAMN VISA, DAMN IT.
。微
【在 h****t 的大作中提到】
: 解释一下名词吧。 什么是combinational equivalence checking?
: 什么是BMC，为什么sequential 太难 ？
好多牛VERIFICATION的会议在欧洲开.
搞的俺PAPER没少发,会一个没参加.
DAMN VISA, DAMN IT.
。微
【在 h****t 的大作中提到】
: 解释一下名词吧。 什么是combinational equivalence checking?
: 什么是BMC，为什么sequential 太难 ？
R*r
21 楼
both are checking software properties ... it depends on how expressive
the type system is
【在 h****t 的大作中提到】
: would that be type checking, instead of model checking?
the type system is
【在 h****t 的大作中提到】
: would that be type checking, instead of model checking?
R*r
22 楼
the science of removing software bugs? ...
【在 T********r 的大作中提到】
: cannot agree more. formal method is always a good thing in academia. it is
: computer *science*, not computer *engineering*. the more I get into it, the
: more I appreciate it.
【在 T********r 的大作中提到】
: cannot agree more. formal method is always a good thing in academia. it is
: computer *science*, not computer *engineering*. the more I get into it, the
: more I appreciate it.
T*r
23 楼
science can be used to solve pratical problems.
【在 R****r 的大作中提到】
: the science of removing software bugs? ...
【在 R****r 的大作中提到】
: the science of removing software bugs? ...
h*t
24 楼
big cft. :)
【在 m****n 的大作中提到】
: 好象欧洲比米国做的好,那儿的大牛不少.
: 好多牛VERIFICATION的会议在欧洲开.
: 搞的俺PAPER没少发,会一个没参加.
: DAMN VISA, DAMN IT.
:
: 。微
【在 m****n 的大作中提到】
: 好象欧洲比米国做的好,那儿的大牛不少.
: 好多牛VERIFICATION的会议在欧洲开.
: 搞的俺PAPER没少发,会一个没参加.
: DAMN VISA, DAMN IT.
:
: 。微
h*t
25 楼
yes. the whole model checking research boils down to how to reduce cost.
【在 R****r 的大作中提到】
: both are checking software properties ... it depends on how expressive
: the type system is
【在 R****r 的大作中提到】
: both are checking software properties ... it depends on how expressive
: the type system is
h*t
26 楼
and find the underlying science behind pratical problems.
【在 T********r 的大作中提到】
: science can be used to solve pratical problems.
【在 T********r 的大作中提到】
: science can be used to solve pratical problems.
相关阅读
有没有人自己买几个服务器或者电脑组装个multiple clusters来跑hadoop？【原创】科技公司的offer该如何选择？ (转载)GT OMSCS 2019 fall 入学 求加入各种相关群想转Java开发，学什么framework最好找工作？ (转载)【找工作】 生物信息学 / 癌症细胞生物学 背景大学是对抗互联网＋的最后堡垒吗？（转载)Data Mining 会议交友群有没有码工微信群啊 (转载)请教个问题，不知发这里是否合适？谢谢选校求助 CS@旧金山大学 VS SE@SJSU商科背景转CS求问Assistant Professor positionCE还是CS的master？请高手帮帮忙，局域网程序运行缓慢，server上 没问题compress data in distributed sensor network帮朋友咨询一下计算机专业博士的学校排名，多谢。近40岁硬工大叔转行CS可行吗？可耻可悲的 上海交大 汉芯造假招中文自然语言处理和生成的兼职 可在家工作请帮忙选下电脑